Use 4byte memory model fot FloatingPoint tests to pass

ultimate-pa · Nov 27, 2024 · 012959b · 012959b
1 parent 860c6cc
commit 012959b
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 0 deletions.
diff --git a/trunk/examples/programs/FloatingPoint/regression/c/AutomizerC-Reach-32bit-WOLF-Float.epf b/trunk/examples/programs/FloatingPoint/regression/c/AutomizerC-Reach-32bit-WOLF-Float.epf
@@ -11,6 +11,7 @@
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/If\ two\ pointers\ are\ subtracted\ or\ compared\ they\ have\ the\ same\ base\ address=IGNORE
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Pointer\ base\ address\ is\ valid\ at\ dereference=IGNORE
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Use\ bitvectors\ instead\ of\ ints=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Memory\ model=HoenickeLindenmann_4ByteResolution
 @de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator=0.0.1
 
 

diff --git a/...ples/programs/FloatingPoint/regression/c/AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf b/...ples/programs/FloatingPoint/regression/c/AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf
@@ -14,6 +14,7 @@
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Use\ constant\ arrays=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Adapt\ memory\ model\ on\ pointer\ casts\ if\ necessary=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Let\ fesetround\ change\ the\ rounding\ mode=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Memory\ model=HoenickeLindenmann_4ByteResolution
 @de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator=0.0.1
 
 

diff --git a/...loatingPoint/regression/c/all/AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf b/...loatingPoint/regression/c/all/AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf
@@ -15,6 +15,7 @@
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Use\ constant\ arrays=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Adapt\ memory\ model\ on\ pointer\ casts\ if\ necessary=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Let\ fesetround\ change\ the\ rounding\ mode=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Memory\ model=HoenickeLindenmann_4ByteResolution
 @de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator=0.0.1
 
 

diff --git a/.../programs/FloatingPoint/regression/cNoRoundingError/AutomizerC-Reach-32bit-WOLF-Float.epf b/.../programs/FloatingPoint/regression/cNoRoundingError/AutomizerC-Reach-32bit-WOLF-Float.epf
@@ -11,6 +11,7 @@
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/If\ two\ pointers\ are\ subtracted\ or\ compared\ they\ have\ the\ same\ base\ address=IGNORE
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Pointer\ base\ address\ is\ valid\ at\ dereference=IGNORE
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Use\ bitvectors\ instead\ of\ ints=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Memory\ model=HoenickeLindenmann_4ByteResolution
 @de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator=0.0.1
 
 

diff --git a/...grams/FloatingPoint/regression/cNoRoundingError/AutomizerC-Reach-32bit-Z3-IcWpLv-Real.epf b/...grams/FloatingPoint/regression/cNoRoundingError/AutomizerC-Reach-32bit-Z3-IcWpLv-Real.epf
@@ -11,6 +11,7 @@
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/If\ two\ pointers\ are\ subtracted\ or\ compared\ they\ have\ the\ same\ base\ address=IGNORE
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Pointer\ base\ address\ is\ valid\ at\ dereference=IGNORE
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Use\ bitvectors\ instead\ of\ ints=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Memory\ model=HoenickeLindenmann_4ByteResolution
 @de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator=0.0.1