Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
was for stateful MC, remove this
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 5 Nov 2023 16:11:07 +0000 (17:11 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 5 Nov 2023 16:11:07 +0000 (17:11 +0100)
docs/source/Tutorial_Model-checking.rst
teshsuite/smpi/MBI/simgrid.py
tools/cmake/MakeLib.cmake

index 998bb44..4e01642 100644 (file)
@@ -308,11 +308,6 @@ If you want to run such analysis on your own code, out of the provided docker, t
 - SimGrid should naturally :ref:`be compiled <install_src>` with model-checking support. This requires a full set of dependencies
   (documented on the :ref:`relevant page <install_src>`) and should not be activated by default as there is a small performance penalty for
   codes using a SimGrid with MC enabled (even if you don't activate the model-checking at run time).
-- You should pass some specific flags to the linker when compiling your application: ``-Wl,-znorelro -Wl,-znoseparate-code`` In the
-  docker, the provided CMakeLists.txt provides them for you when compiling the provided code. ``smpicc`` and friends also add this
-  parameter automatically.
-- If you get error messages complaining about the Dwarf version used, try adding ``-gdwarf-4`` to you CFLAGS and CXXFLAGS.
-  If you find a situation where this flag is needed in ``smpicc``, please report this issue.
 - Also install ``libboost-stacktrace-dev`` to display nice backtraces from the application side (the one from the model-checking side is
   available in any case, but it contains less details).
 - Mc SimGrid uses the ``ptrace`` system call to spy on the verified application. Some versions of Docker forbid the use of this call by
index 3c1ca88..907abc8 100644 (file)
@@ -55,7 +55,7 @@ class Tool(mbi.AbstractTool):
         execcmd = execcmd.replace('$infty_buffer', "--cfg=smpi/buffering:infty")
 
         mbi.run_cmd(
-            buildcmd=f"smpicc {filename} -trace-call-location -g -Wl,-znorelro -Wl,-znoseparate-code -o {binary}",
+            buildcmd=f"smpicc {filename} -trace-call-location -g -o {binary}",
             execcmd=execcmd,
             cachefile=cachefile,
             filename=filename,
index e66769d..b91be7d 100644 (file)
@@ -173,10 +173,6 @@ if(CMAKE_COMPILER_IS_GNUCC AND GCCLIBATOMIC_LIBRARY)
 endif()
 mark_as_advanced(GCCLIBATOMIC_LIBRARY)
 
-if(enable_model-checking AND (NOT LINKER_VERSION VERSION_LESS "2.30"))
-    set(SIMGRID_DEP   "${SIMGRID_DEP}   -Wl,-znorelro -Wl,-znoseparate-code")
-endif()
-
 target_link_libraries(simgrid  ${SIMGRID_DEP})
 
 # Dependencies from maintainer mode