diff --git a/regression-tests/acsl-contracts/Answers b/regression-tests/acsl-contracts/Answers index d33f440..8164465 100644 --- a/regression-tests/acsl-contracts/Answers +++ b/regression-tests/acsl-contracts/Answers @@ -30,15 +30,12 @@ contract10.hcc SAFE contract11.hcc -Warning: enabling heap model SAFE contract12.hcc -Warning: enabling heap model SAFE contract13.hcc -Warning: enabling heap model UNSAFE contract14.hcc @@ -48,7 +45,6 @@ contract15.hcc SAFE contract16.hcc -Warning: enabling heap model SAFE contract17.hcc @@ -58,11 +54,9 @@ contract18.hcc UNSAFE contract19.hcc -Warning: enabling heap model SAFE contract20.hcc -Warning: enabling heap model UNSAFE contract21.hcc @@ -72,23 +66,18 @@ contract22.hcc UNSAFE contract23.hcc -Warning: enabling heap model UNSAFE contract24.hcc -Warning: enabling heap model UNSAFE contract25.hcc -Warning: enabling heap model SAFE contract26.hcc -Warning: enabling heap model SAFE contract27.hcc -Warning: enabling heap model SAFE struct-field-access-1-true.hcc diff --git a/regression-tests/acsl-standalone/Answers b/regression-tests/acsl-standalone/Answers index af881c3..c5e2a89 100644 --- a/regression-tests/acsl-standalone/Answers +++ b/regression-tests/acsl-standalone/Answers @@ -3,243 +3,233 @@ inc_safe.c SAFE inc_unsafe.c -UNSAFE ------------------- +------------------------------------------ Init: - foo1_1(0, 0) ------------------- - | - | - V - foo6_10(0, 0, 0) ------------------- + foo1_1(nthAddr(0), 0, nthAddr(0), 0) +------------------------------------------ + | + | + V + foo6_10(nthAddr(0), 0, nthAddr(0), 0, 0) +------------------------------------------ Final: - foo6_10(0, 0, 0) ------------------- + foo6_10(nthAddr(0), 0, nthAddr(0), 0, 0) +------------------------------------------ Failed assertion: -false :- foo6_10(x, x_old, _res1), _res1 < 1. (line:3 col:19) +false :- foo6_10(@v_cleanup, x, @v_cleanup_old, x_old, _res1), _res1 < 1. (line:3 col:19) (property: postcondition of function foo asserted at 1:1.) +UNSAFE mc91_safe.c SAFE mc91_unsafe.c -UNSAFE ------------------------- +------------------------------------------------ Init: - foo1_1(90, 90) ------------------------- - | - | - V - foo8_10(90, 90) ------------------------- - | - | - V - foo9_12_0(90, 90, 102) ------------------------- - | - | - V - foo9_12(90, 90, 92) ------------------------- + foo1_1(nthAddr(0), 90, nthAddr(0), 90) +------------------------------------------------ + | + | + V + foo8_10(nthAddr(0), 90, nthAddr(0), 90) +------------------------------------------------ + | + | + V + foo9_12_0(nthAddr(0), 90, nthAddr(0), 90, 102) +------------------------------------------------ + | + | + V + foo9_12(nthAddr(0), 90, nthAddr(0), 90, 92) +------------------------------------------------ Final: - foo9_12(90, 90, 92) ------------------------- + foo9_12(nthAddr(0), 90, nthAddr(0), 90, 92) +------------------------------------------------ Failed assertion: -false :- foo9_12(n, n_old, _res1), !((100 < n_old | _res1 = 91) & (n_old - 101 < 1 | _res1 = n_old - 10)). (line:2 col:4) +false :- foo9_12(@v_cleanup, n, @v_cleanup_old, n_old, _res1), !((100 < n_old | _res1 = 91) & (n_old - 101 < 1 | _res1 = n_old - 10)). (line:2 col:4) (property: postcondition of function foo asserted at 1:1.) +UNSAFE incdec_safe.c SAFE incdec_unsafe.c -UNSAFE ----------------------- +---------------------------------------------- Init: - foo15_1(0, 0) ----------------------- - | - | - V - foo19_10_0(0, 0, -1) ----------------------- - | - | - V - foo19_10(0, 0, 1) ----------------------- + foo15_1(nthAddr(0), 0, nthAddr(0), 0) +---------------------------------------------- + | + | + V + foo19_10_0(nthAddr(0), 0, nthAddr(0), 0, -1) +---------------------------------------------- + | + | + V + foo19_10(nthAddr(0), 0, nthAddr(0), 0, 1) +---------------------------------------------- Final: - foo19_10(0, 0, 1) ----------------------- + foo19_10(nthAddr(0), 0, nthAddr(0), 0, 1) +---------------------------------------------- Failed assertion: -false :- foo19_10(n, n_old, _res3), _res3 != n_old. (line:16 col:4) +false :- foo19_10(@v_cleanup, n, @v_cleanup_old, n_old, _res3), _res3 != n_old. (line:16 col:4) (property: postcondition of function foo asserted at 15:1.) +UNSAFE getptr_safe.c -Warning: enabling heap model +Warning: A property file exists, but properties are also specified in the command-line. Ignoring the property file. SAFE getptr_unsafe.c -Warning: enabling heap model -UNSAFE +Warning: A property file exists, but properties are also specified in the command-line. Ignoring the property file. ------------------------------------------------------- +------------------------------------------------------------------------------ Init: - foo1_1(emptyHeap, nthAddr(0), emptyHeap, nthAddr(0)) ------------------------------------------------------- + foo1_1(emptyHeap, nthAddr(0), nthAddr(0), emptyHeap, nthAddr(0), nthAddr(0)) +------------------------------------------------------------------------------ Final: - foo1_1(emptyHeap, nthAddr(0), emptyHeap, nthAddr(0)) ------------------------------------------------------- + foo1_1(emptyHeap, nthAddr(0), nthAddr(0), emptyHeap, nthAddr(0), nthAddr(0)) +------------------------------------------------------------------------------ Failed assertion: -false :- foo1_1(@h, p, @h_old, p_old), !is_O_Int(read(@h, p)). (line:4 col:9) +false :- foo1_1(@h, @v_cleanup, p, @h_old, @v_cleanup_old, p_old), !is_O_Int(read(@h, p)). (line:4 col:9) (property: valid-deref) +UNSAFE assigns_safe.c -Warning: enabling heap model SAFE assigns_unsafe.c -Warning: enabling heap model -UNSAFE ------------------------------------------------------------------------------------------------------------------ +----------------------------------------------------------------------------------------------------------------------------------------- Init: - foo1_1(newHeap(alloc(emptyHeap, O_Int(47))), nthAddr(1), newHeap(alloc(emptyHeap, O_Int(47))), nthAddr(1)) ------------------------------------------------------------------------------------------------------------------ - | - | - V - foo8_10(newHeap(alloc(emptyHeap, O_Int(42))), nthAddr(1), newHeap(alloc(emptyHeap, O_Int(47))), nthAddr(1), 42) ------------------------------------------------------------------------------------------------------------------ + foo1_1(newHeap(alloc(emptyHeap, O_Int(47))), nthAddr(0), nthAddr(1), newHeap(alloc(emptyHeap, O_Int(47))), nthAddr(0), nthAddr(1)) +----------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo8_10(newHeap(alloc(emptyHeap, O_Int(42))), nthAddr(0), nthAddr(1), newHeap(alloc(emptyHeap, O_Int(47))), nthAddr(0), nthAddr(1), 42) +----------------------------------------------------------------------------------------------------------------------------------------- Final: - foo8_10(newHeap(alloc(emptyHeap, O_Int(42))), nthAddr(1), newHeap(alloc(emptyHeap, O_Int(47))), nthAddr(1), 42) ------------------------------------------------------------------------------------------------------------------ + foo8_10(newHeap(alloc(emptyHeap, O_Int(42))), nthAddr(0), nthAddr(1), newHeap(alloc(emptyHeap, O_Int(47))), nthAddr(0), nthAddr(1), 42) +----------------------------------------------------------------------------------------------------------------------------------------- Failed assertion: -false :- foo8_10(@h, p, @h_old, p_old, _res1), !(_res1 = 42 & @h = @h_old). (line:4 col:20) +false :- foo8_10(@h, @v_cleanup, p, @h_old, @v_cleanup_old, p_old, _res1), !(_res1 = 42 & @h = @h_old & @v_cleanup = @v_cleanup_old). (line:4 col:20) (property: postcondition of function foo asserted at 1:1.) +UNSAFE maxptr_safe.c -Warning: enabling heap model SAFE maxptr_unsafe.c -Warning: enabling heap model -UNSAFE -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Init: - foo1_1(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(1), nthAddr(2)) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo8_17(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(1), nthAddr(2)) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo11_12(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(1), nthAddr(2), 5) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + foo1_1(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(0), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(0), nthAddr(1), nthAddr(2)) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo8_17(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(0), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(0), nthAddr(1), nthAddr(2)) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo11_12(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(0), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(0), nthAddr(1), nthAddr(2), 5) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Final: - foo11_12(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(1), nthAddr(2), 5) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + foo11_12(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(0), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nthAddr(0), nthAddr(1), nthAddr(2), 5) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Failed assertion: -false :- foo11_12(@h, p, q, @h_old, p_old, q_old, _res1), !((_res1 = getInt(read(@h, p_old)) | _res1 = getInt(read(@h, q_old))) & _res1 >= getInt(read(@h, p_old)) & _res1 >= getInt(read(@h, q_old))). (line:3 col:25) +false :- foo11_12(@h, @v_cleanup, p, q, @h_old, @v_cleanup_old, p_old, q_old, _res1), !((_res1 = getInt(read(@h, p_old)) | _res1 = getInt(read(@h, q_old))) & _res1 >= getInt(read(@h, p_old)) & _res1 >= getInt(read(@h, q_old))). (line:3 col:25) (property: postcondition of function foo asserted at 1:1.) +UNSAFE old_safe.c -Warning: enabling heap model SAFE old_unsafe.c -Warning: enabling heap model -UNSAFE ----------------------------------------------------------------------------------------------------------------------- +---------------------------------------------------------------------------------------------------------------------------------------------- Init: - foo4_1(newHeap(alloc(emptyHeap, O_Int(46))), -42, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(46))), -42, nthAddr(1)) ----------------------------------------------------------------------------------------------------------------------- - | - | - V - foo(newHeap(alloc(emptyHeap, O_Int(42))), -42, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(46))), -42, nthAddr(1)) ----------------------------------------------------------------------------------------------------------------------- - | - | - V - foo10_8(newHeap(alloc(emptyHeap, O_Int(42))), 0, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(46))), -42, nthAddr(1)) ----------------------------------------------------------------------------------------------------------------------- + foo4_1(newHeap(alloc(emptyHeap, O_Int(46))), nthAddr(0), -42, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(46))), nthAddr(0), -42, nthAddr(1)) +---------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo(newHeap(alloc(emptyHeap, O_Int(42))), nthAddr(0), -42, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(46))), nthAddr(0), -42, nthAddr(1)) +---------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo10_8(newHeap(alloc(emptyHeap, O_Int(42))), nthAddr(0), 0, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(46))), nthAddr(0), -42, nthAddr(1)) +---------------------------------------------------------------------------------------------------------------------------------------------- Final: - foo10_8(newHeap(alloc(emptyHeap, O_Int(42))), 0, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(46))), -42, nthAddr(1)) ----------------------------------------------------------------------------------------------------------------------- + foo10_8(newHeap(alloc(emptyHeap, O_Int(42))), nthAddr(0), 0, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(46))), nthAddr(0), -42, nthAddr(1)) +---------------------------------------------------------------------------------------------------------------------------------------------- Failed assertion: -false :- foo10_8(@h, g, p, @h_old, g_old, p_old), g != g_old + getInt(read(@h_old, p_old)). (line:6 col:22) +false :- foo10_8(@h, @v_cleanup, g, p, @h_old, @v_cleanup_old, g_old, p_old), g != g_old + getInt(read(@h_old, p_old)). (line:6 col:22) (property: postcondition of function foo asserted at 4:1.) +UNSAFE dblptr-assigns_safe.c -Warning: enabling heap model SAFE dblptr-assigns_unsafe.c -Warning: enabling heap model -UNSAFE --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- +-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Init: - foo5_1(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), 0, nthAddr(3), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), 0, nthAddr(3), nthAddr(2)) --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(42))), 0, nthAddr(3), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), 0, nthAddr(3), nthAddr(2)) --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo14_9(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(42))), O_Addr(nthAddr(1)))), O_Int(42))), 42, nthAddr(3), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), 0, nthAddr(3), nthAddr(2)) --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + foo5_1(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), nthAddr(0), 0, nthAddr(3), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), nthAddr(0), 0, nthAddr(3), nthAddr(2)) +-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(42))), nthAddr(0), 0, nthAddr(3), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), nthAddr(0), 0, nthAddr(3), nthAddr(2)) +-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo14_9(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(42))), O_Addr(nthAddr(1)))), O_Int(42))), nthAddr(0), 42, nthAddr(3), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), nthAddr(0), 0, nthAddr(3), nthAddr(2)) +-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Final: - foo14_9(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(42))), O_Addr(nthAddr(1)))), O_Int(42))), 42, nthAddr(3), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), 0, nthAddr(3), nthAddr(2)) --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + foo14_9(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(42))), O_Addr(nthAddr(1)))), O_Int(42))), nthAddr(0), 42, nthAddr(3), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), nthAddr(0), 0, nthAddr(3), nthAddr(2)) +-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Failed assertion: -false :- foo14_9(@h, g, p, q, @h_old, g_old, p_old, q_old), !(!(_p != q_old & _p != p_old) | read(@h, _p) = read(@h_old, _p)). (line:6 col:4) +false :- foo14_9(@h, @v_cleanup, g, p, q, @h_old, @v_cleanup_old, g_old, p_old, q_old), !((!(_p != q_old & _p != p_old) | read(@h, _p) = read(@h_old, _p)) & @v_cleanup = @v_cleanup_old). (line:6 col:4) (property: postcondition of function foo asserted at 5:1.) +UNSAFE swap_safe.c -Warning: enabling heap model SAFE swap_unsafe.c -Warning: enabling heap model -UNSAFE ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- +---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Init: - foo3_1(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nthAddr(1), nthAddr(2)) ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo10_3(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nthAddr(1), nthAddr(2), 7) ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo(newHeap(alloc(newBatchHeap(batchAlloc(emptyHeap, O_Int(9), 2)), O_Int(0))), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nthAddr(1), nthAddr(2), 7) ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo12_8(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(9))), O_Int(7))), O_Int(0))), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nthAddr(1), nthAddr(2)) ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + foo3_1(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nthAddr(0), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nthAddr(0), nthAddr(1), nthAddr(2)) +---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo10_3(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nthAddr(0), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nthAddr(0), nthAddr(1), nthAddr(2), 7) +---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo(newHeap(alloc(newBatchHeap(batchAlloc(emptyHeap, O_Int(9), 2)), O_Int(0))), nthAddr(0), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nthAddr(0), nthAddr(1), nthAddr(2), 7) +---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo12_8(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(9))), O_Int(7))), O_Int(0))), nthAddr(0), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nthAddr(0), nthAddr(1), nthAddr(2)) +---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Final: - foo12_8(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(9))), O_Int(7))), O_Int(0))), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nthAddr(1), nthAddr(2)) ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + foo12_8(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(9))), O_Int(7))), O_Int(0))), nthAddr(0), nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nthAddr(0), nthAddr(1), nthAddr(2)) +---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Failed assertion: -false :- foo12_8(@h, a, b, @h_old, a_old, b_old), !(getInt(read(@h, a_old)) = getInt(read(@h_old, b_old)) & getInt(read(@h, b_old)) = getInt(read(@h, a_old)) & (!(_p != a_old & _p != b_old) | read(@h, _p) = read(@h_old, _p))). (line:6 col:19) +false :- foo12_8(@h, @v_cleanup, a, b, @h_old, @v_cleanup_old, a_old, b_old), !(getInt(read(@h, a_old)) = getInt(read(@h_old, b_old)) & getInt(read(@h, b_old)) = getInt(read(@h, a_old)) & (!(_p != a_old & _p != b_old) | read(@h, _p) = read(@h_old, _p)) & @v_cleanup = @v_cleanup_old). (line:6 col:19) (property: postcondition of function foo asserted at 3:1.) +UNSAFE diff --git a/regression-tests/horn-hcc-heap/memtrack-04.yml b/regression-tests/acsl-standalone/getptr_safe.yml similarity index 72% rename from regression-tests/horn-hcc-heap/memtrack-04.yml rename to regression-tests/acsl-standalone/getptr_safe.yml index 9492d7c..5d069d6 100644 --- a/regression-tests/horn-hcc-heap/memtrack-04.yml +++ b/regression-tests/acsl-standalone/getptr_safe.yml @@ -1,11 +1,10 @@ format_version: '2.0' -input_files: 'memtrack-04.c' +input_files: 'getptr_safe.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: true - subproperty: valid-memtrack options: language: C diff --git a/regression-tests/horn-hcc-heap/memtrack-05.yml b/regression-tests/acsl-standalone/getptr_unsafe.yml similarity index 72% rename from regression-tests/horn-hcc-heap/memtrack-05.yml rename to regression-tests/acsl-standalone/getptr_unsafe.yml index b325b9f..454b57d 100644 --- a/regression-tests/horn-hcc-heap/memtrack-05.yml +++ b/regression-tests/acsl-standalone/getptr_unsafe.yml @@ -1,11 +1,11 @@ format_version: '2.0' -input_files: 'memtrack-05.c' +input_files: 'getptr_unsafe.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: false - subproperty: valid-memtrack + subproperty: valid-deref options: language: C diff --git a/regression-tests/acsl-standalone/runtests b/regression-tests/acsl-standalone/runtests index bb0d8d2..fa48d98 100755 --- a/regression-tests/acsl-standalone/runtests +++ b/regression-tests/acsl-standalone/runtests @@ -24,6 +24,6 @@ TESTS="inc_safe.c \ for name in $TESTS; do echo echo $name - $LAZABS "$@" $name 2>&1 | grep -v 'at ' + $LAZABS "$@" $name -memsafety -reachsafety done diff --git a/regression-tests/horn-bv/Answers b/regression-tests/horn-bv/Answers index 5ffc01b..8e22889 100644 --- a/regression-tests/horn-bv/Answers +++ b/regression-tests/horn-bv/Answers @@ -1,7 +1,6 @@ nonlinear2.hcc Warning: no definition of function "nondet" available -UNSAFE ----------------------------------------------------------------- Init: @@ -66,8 +65,9 @@ Final: main((-447365120).\as[signed bv[32]], 11.\as[signed bv[32]]) ----------------------------------------------------------------- Failed assertion: -false :- main(f:5, i:6), f:5 < 1 | i:6 < 1. (line:13 col:3) +false :- main(f:5, i:6), f:5 < 1 | i:6 < 1. (line:13 col:3) (property: user-assertion) +UNSAFE ../horn-hcc/loop1.hcc Warning: entry function "main" not found diff --git a/regression-tests/horn-contracts/Answers b/regression-tests/horn-contracts/Answers index e7796bc..a1557e9 100644 --- a/regression-tests/horn-contracts/Answers +++ b/regression-tests/horn-contracts/Answers @@ -1,6 +1,5 @@ contract1.hcc -SAFE Inferred ACSL annotations ================================================================================ @@ -11,9 +10,9 @@ Inferred ACSL annotations */ ================================================================================ +SAFE contract2.hcc -SAFE Inferred ACSL annotations ================================================================================ @@ -24,9 +23,9 @@ Inferred ACSL annotations */ ================================================================================ +SAFE contract2b.hcc -UNSAFE ------------------ Init: @@ -51,11 +50,11 @@ Final: main_2(-4, 5) ------------------ Failed assertion: -false :- main_2(g:2, y:14), g:2 < 0. (line:18 col:3) +false :- main_2(g:2, y:14), g:2 < 0. (line:18 col:3) (property: user-assertion) +UNSAFE contract3.hcc -SAFE Inferred ACSL annotations ================================================================================ @@ -66,9 +65,9 @@ Inferred ACSL annotations */ ================================================================================ +SAFE takeuchi.hcc -SAFE Inferred ACSL annotations ================================================================================ @@ -79,9 +78,9 @@ Inferred ACSL annotations */ ================================================================================ +SAFE assert.hcc -SAFE Inferred ACSL annotations ================================================================================ @@ -92,9 +91,9 @@ Inferred ACSL annotations */ ================================================================================ +SAFE fib.hcc -UNSAFE --------------- Init: @@ -109,8 +108,11 @@ Final: main12_3_1(8) --------------- Failed assertion: -false :- main12_3_1(x:12), x:12 != 0. (line:14 col:3) +false :- main12_3_1(x:12), x:12 != 0. (line:14 col:3) (property: user-assertion) +UNSAFE stackptr.hcc -Warning: enabling heap model +tricera.concurrency.ccreader.CCExceptions$TranslationException: Function contracts are currently not supported together with stack pointers (10:5) +(error "Function contracts are currently not supported together with stack pointers (10:5)") +Other Error: Function contracts are currently not supported together with stack pointers (10:5) diff --git a/regression-tests/horn-hcc-2/Answers b/regression-tests/horn-hcc-2/Answers index 879874d..7f7205a 100644 --- a/regression-tests/horn-hcc-2/Answers +++ b/regression-tests/horn-hcc-2/Answers @@ -38,7 +38,6 @@ Warning: entry function "main" not found SAFE lazy-and-or-bug.hcc -UNSAFE ------------------------------------ Init: @@ -62,6 +61,7 @@ Init: Final: A10_7(1) main(1, 1) ------------------------------------ +UNSAFE channels.hcc Warning: entry function "main" not found @@ -73,7 +73,6 @@ SAFE channels-2b.hcc Warning: entry function "main" not found -UNSAFE ------------------------ Init: @@ -88,6 +87,7 @@ Init: Final: A7_10(42) B(42, -10) ------------------------ +UNSAFE channels-3.hcc tricera.concurrency.ccreader.CCExceptions$TranslationException: Cannot execute Receive(d) and Send(c) in one step @@ -100,7 +100,6 @@ SAFE duration2.hcc Warning: enabling time -UNSAFE ------------------------------------------------------ Init: @@ -130,6 +129,7 @@ Init: Final: A_2(0, 1, 0, 0, 0, 0) main_1(0, 1, 0, 0, 0, 0) ------------------------------------------------------ +UNSAFE duration3.hcc Warning: enabling time @@ -137,7 +137,6 @@ SAFE duration3b.hcc Warning: enabling time -UNSAFE ------------------------------------------------ Init: @@ -167,6 +166,7 @@ Init: Final: B_2(0, 1, 0, 0, 0) main9_15_0(0, 1, 0, 0) ------------------------------------------------ +UNSAFE duration3c.hcc Warning: enabling time @@ -174,7 +174,6 @@ SAFE duration3d.hcc Warning: enabling time -UNSAFE ---------------------------------------------- Init: @@ -206,6 +205,7 @@ Delay: 1.0 Final: B_2(0, 1, 0, -1) main9_15_0(0, 1, 0) ---------------------------------------------- +UNSAFE nonlinear1.hcc Warning: no definition of function "nondet" available @@ -213,7 +213,6 @@ SAFE nonlinear2.hcc Warning: no definition of function "nondet" available -UNSAFE ---------------- Init: @@ -228,14 +227,14 @@ Final: main12_7(2, 4) ---------------- Failed assertion: -false :- main12_7(x:7, y:10). (line:13 col:5) +false :- main12_7(x:7, y:10). (line:13 col:5) (property: user-assertion) +UNSAFE typedef1.hcc SAFE switch1.hcc -UNSAFE ---------------- Init: @@ -250,8 +249,9 @@ Final: main(0, 0) ---------------- Failed assertion: -false :- main(x:4, y:5), y:5 < 1. (line:19 col:3) +false :- main(x:4, y:5), y:5 < 1. (line:19 col:3) (property: user-assertion) +UNSAFE switch2.hcc Warning: no definition of function "nondet" available diff --git a/regression-tests/horn-hcc-array/Answers b/regression-tests/horn-hcc-array/Answers index 19bede9..85f49ae 100644 --- a/regression-tests/horn-hcc-array/Answers +++ b/regression-tests/horn-hcc-array/Answers @@ -1,114 +1,85 @@ out-of-bounds-line1.c -Warning: enabling heap model Warning: no definition of function "nondet" available -UNSAFE ---------------------------------------------------------------------------- +--------------------------------------------------------------------------------------- Init: - main9_3(emptyHeap, AddrRange(nthAddr(0), 0)) ---------------------------------------------------------------------------- - | - | - V - main_2(newHeap(alloc(emptyHeap, O_Int(10))), AddrRange(nthAddr(1), 1), 1) ---------------------------------------------------------------------------- + main9_3(emptyHeap, nthAddr(0), AddrRange(nthAddr(0), 0)) +--------------------------------------------------------------------------------------- + | + | + V + main_2(newHeap(alloc(emptyHeap, O_Int(10))), nthAddr(0), AddrRange(nthAddr(1), 1), 1) +--------------------------------------------------------------------------------------- Final: - main_2(newHeap(alloc(emptyHeap, O_Int(10))), AddrRange(nthAddr(1), 1), 1) ---------------------------------------------------------------------------- + main_2(newHeap(alloc(emptyHeap, O_Int(10))), nthAddr(0), AddrRange(nthAddr(1), 1), 1) +--------------------------------------------------------------------------------------- Failed assertion: -false :- main_2(@h, a:6, n:9), !is_O_Int(read(@h, nthAddrRange(a:6, n:9))). (line:6 col:5) +false :- main_2(@h, @v_cleanup, a:6, n:9), !is_O_Int(read(@h, nthAddrRange(a:6, n:9))). (line:6 col:5) (property: valid-deref) -valid-memsafety - expected verdict matches the result! +UNSAFE out-of-bounds-line2.c -Warning: enabling heap model -UNSAFE ------------------------------------------------------------------------------------------ +----------------------------------------------------------------------------------------------------- Init: - main7_3_1(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 42)), AddrRange(nthAddr(1), 42)) ------------------------------------------------------------------------------------------ + main7_3_1(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 42)), nthAddr(0), AddrRange(nthAddr(1), 42)) +----------------------------------------------------------------------------------------------------- Final: - main7_3_1(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 42)), AddrRange(nthAddr(1), 42)) ------------------------------------------------------------------------------------------ + main7_3_1(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 42)), nthAddr(0), AddrRange(nthAddr(1), 42)) +----------------------------------------------------------------------------------------------------- Failed assertion: -false :- main7_3_1(@h, a:4), !is_O_Int(read(@h, nthAddrRange(a:4, 42))). (line:4 col:5) +false :- main7_3_1(@h, @v_cleanup, a:4), !is_O_Int(read(@h, nthAddrRange(a:4, 42))). (line:4 col:5) (property: valid-deref) -valid-memsafety - expected verdict matches the result! +UNSAFE out-of-bounds-line3.c -Warning: enabling heap model Warning: no definition of function "nondet" available -UNSAFE ---------------------------------------------------------------------------- +--------------------------------------------------------------------------------------- Init: - main9_3(emptyHeap, AddrRange(nthAddr(0), 0)) ---------------------------------------------------------------------------- - | - | - V - main_2(newHeap(alloc(emptyHeap, O_Int(10))), AddrRange(nthAddr(1), 1), 1) ---------------------------------------------------------------------------- + main9_3(emptyHeap, nthAddr(0), AddrRange(nthAddr(0), 0)) +--------------------------------------------------------------------------------------- + | + | + V + main_2(newHeap(alloc(emptyHeap, O_Int(10))), nthAddr(0), AddrRange(nthAddr(1), 1), 1) +--------------------------------------------------------------------------------------- Final: - main_2(newHeap(alloc(emptyHeap, O_Int(10))), AddrRange(nthAddr(1), 1), 1) ---------------------------------------------------------------------------- + main_2(newHeap(alloc(emptyHeap, O_Int(10))), nthAddr(0), AddrRange(nthAddr(1), 1), 1) +--------------------------------------------------------------------------------------- Failed assertion: -false :- main_2(@h, a:6, n:9), !is_O_Int(read(@h, nthAddrRange(a:6, n:9))). (line:6 col:5) +false :- main_2(@h, @v_cleanup, a:6, n:9), !is_O_Int(read(@h, nthAddrRange(a:6, n:9))). (line:6 col:5) (property: valid-deref) -valid-memsafety - expected verdict matches the result! +UNSAFE out-of-bounds-line4.c -Warning: enabling heap model -UNSAFE ---------------------------------------------------------------------------------------- +--------------------------------------------------------------------------------------------------- Init: - main7_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 42)), AddrRange(nthAddr(1), 42)) ---------------------------------------------------------------------------------------- + main7_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 42)), nthAddr(0), AddrRange(nthAddr(1), 42)) +--------------------------------------------------------------------------------------------------- Final: - main7_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 42)), AddrRange(nthAddr(1), 42)) ---------------------------------------------------------------------------------------- + main7_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 42)), nthAddr(0), AddrRange(nthAddr(1), 42)) +--------------------------------------------------------------------------------------------------- Failed assertion: -false :- main7_3(@h, a:4), !is_O_Int(read(@h, nthAddrRange(a:4, -1*1))). (line:4 col:5) +false :- main7_3(@h, @v_cleanup, a:4), !is_O_Int(read(@h, nthAddrRange(a:4, -1*1))). (line:4 col:5) (property: valid-deref) -valid-memsafety - expected verdict matches the result! +UNSAFE dynamic-loop1.c -Warning: enabling heap model SAFE -valid-memsafety - expected verdict matches the result! -unreach-call - expected verdict matches the result! simple-dynamic-array.c -Warning: enabling heap model SAFE -valid-memsafety - expected verdict matches the result! -unreach-call - expected verdict matches the result! simple-global-array.c -Warning: enabling heap model SAFE -valid-memsafety - expected verdict matches the result! -unreach-call - expected verdict matches the result! array-single-alloc.c -Warning: enabling heap model SAFE array-inside-struct-1.c -UNSAFE --------------------------------------------------------------------------------- Init: @@ -117,22 +88,27 @@ Init: | | V - main15_36_1(S(const(4)), 0) + main15_36(S(const(4)), 0) --------------------------------------------------------------------------------- | | V - main15_36_1(S(store(const(4), 0, 0)), 1) + main15_36(S(store(const(4), 0, 0)), 1) --------------------------------------------------------------------------------- | | V - main15_36_1(S(store(store(const(4), 0, 0), 1, 1)), 2) + main15_36(S(store(store(const(4), 0, 0), 1, 1)), 2) --------------------------------------------------------------------------------- | | V - main15_36_1(S(store(store(store(const(4), 0, 0), 1, 1), 2, 2)), 3) + main15_36(S(store(store(store(const(4), 0, 0), 1, 1), 2, 2)), 3) +--------------------------------------------------------------------------------- + | + | + V + main15_36(S(store(store(store(store(const(4), 0, 0), 1, 1), 2, 2), 3, 3)), 4) --------------------------------------------------------------------------------- | | @@ -143,85 +119,111 @@ Final: main18_36_3(S(store(store(store(store(const(4), 0, 0), 1, 1), 2, 2), 3, 3)), 0) --------------------------------------------------------------------------------- Failed assertion: -false :- main18_36_3(s:14, i:18), select(data(s:14), i:18) = i:18. (line:19 col:5) +false :- main18_36_3(s:14, i:18), select(data(s:14), i:18) = i:18. (line:19 col:5) (property: user-assertion) +UNSAFE pointer-arith-1-safe.c -Warning: enabling heap model SAFE pointer-arith-1-unsafe.c -Warning: enabling heap model -UNSAFE ------------------------------------------------------------------------------------------------------------------------- +------------------------------------------------------------------------------------------------------------------------------------ Init: - main5_3(emptyHeap, AddrRange(nthAddr(0), 0), 2) ------------------------------------------------------------------------------------------------------------------------- - | - | - V - main7_36_2(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(1), 2), 0) ------------------------------------------------------------------------------------------------------------------------- - | - | - V - main7_36_2(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(2), 1), 1) ------------------------------------------------------------------------------------------------------------------------- - | - | - V - main7_36_2(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(0), 0), 2) ------------------------------------------------------------------------------------------------------------------------- + main5_3(emptyHeap, nthAddr(0), AddrRange(nthAddr(0), 0), 2) +------------------------------------------------------------------------------------------------------------------------------------ + | + | + V + main7_36_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), nthAddr(0), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(1), 2), 0) +------------------------------------------------------------------------------------------------------------------------------------ + | + | + V + main7_36_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), nthAddr(0), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(2), 1), 1) +------------------------------------------------------------------------------------------------------------------------------------ + | + | + V + main7_36_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), nthAddr(0), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(0), 0), 2) +------------------------------------------------------------------------------------------------------------------------------------ Final: - main7_36_2(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(0), 0), 2) ------------------------------------------------------------------------------------------------------------------------- + main7_36_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), nthAddr(0), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(0), 0), 2) +------------------------------------------------------------------------------------------------------------------------------------ Failed assertion: -false :- main7_36_2(@h, a:1, n:4, p:6, i:7), !is_O_Int(read(@h, nthAddrRange(p:6, 0))). (line:6 col:7) +false :- main7_36_3(@h, @v_cleanup, a:1, n:4, p:6, i:7), !is_O_Int(read(@h, nthAddrRange(p:6, 0))). (line:6 col:7) (property: valid-deref) +UNSAFE pointer-arith-2-safe.c -Warning: enabling heap model SAFE pointer-arith-2-unsafe.c -Warning: enabling heap model + +------------------------------------------------------------------------------------------------------------------------------------ +Init: + main5_3(emptyHeap, nthAddr(0), AddrRange(nthAddr(0), 0), 2) +------------------------------------------------------------------------------------------------------------------------------------ + | + | + V + main7_36_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), nthAddr(0), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(1), 2), 0) +------------------------------------------------------------------------------------------------------------------------------------ + | + | + V + main7_36_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), nthAddr(0), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(2), 1), 1) +------------------------------------------------------------------------------------------------------------------------------------ + | + | + V + main7_36_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), nthAddr(0), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(0), 0), 2) +------------------------------------------------------------------------------------------------------------------------------------ +Final: + main7_36_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), nthAddr(0), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(0), 0), 2) +------------------------------------------------------------------------------------------------------------------------------------ +Failed assertion: +false :- main7_36_3(@h, @v_cleanup, a:1, n:4, p:6, i:7), !is_O_Int(read(@h, nthAddrRange(p:6, 0))). (line:6 col:7) (property: valid-deref) + UNSAFE ------------------------------------------------------------------------------------------------------------------------- +global-struct-array-1.c + +------------------------------------------------------------------------------------------------------ Init: - main5_3(emptyHeap, AddrRange(nthAddr(0), 0), 2) ------------------------------------------------------------------------------------------------------------------------- - | - | - V - main7_36_2(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(1), 2), 0) ------------------------------------------------------------------------------------------------------------------------- - | - | - V - main7_36_2(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(2), 1), 1) ------------------------------------------------------------------------------------------------------------------------- - | - | - V - main7_36_2(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(0), 0), 2) ------------------------------------------------------------------------------------------------------------------------- + main8_3(newHeap(alloc(newHeap(alloc(emptyHeap, O_S(S(10)))), O_S(S(20)))), AddrRange(nthAddr(1), 2)) +------------------------------------------------------------------------------------------------------ Final: - main7_36_2(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(0), 0), 2) ------------------------------------------------------------------------------------------------------------------------- + main8_3(newHeap(alloc(newHeap(alloc(emptyHeap, O_S(S(10)))), O_S(S(20)))), AddrRange(nthAddr(1), 2)) +------------------------------------------------------------------------------------------------------ Failed assertion: -false :- main7_36_2(@h, a:1, n:4, p:6, i:7), !is_O_Int(read(@h, nthAddrRange(p:6, 0))). (line:6 col:7) +false :- main8_3(@h, sArr:5), f(getS(read(@h, nthAddrRange(sArr:5, 0)))) != 0. (line:8 col:3) (property: user-assertion) +UNSAFE + +array-of-ptr-1.c +SAFE + +simple-global-memsafety1.c +SAFE + +simple-alloca-memsafety1.c +SAFE + +simple-alloca-memsafety2.c +SAFE pointer-arith-3-safe.c -Warning: enabling heap model +Splitting properties: {valid-deref,valid-memtrack,valid-free,unreach-call} + valid-deref... SAFE + valid-memtrack... SAFE + valid-free... SAFE + unreach-call... SAFE SAFE pointer-arith-3-unsafe.c -Warning: enabling heap model -UNSAFE - +Splitting properties: {valid-deref,valid-memtrack,valid-free,unreach-call} + valid-deref... ------------------------------------------------------------------------------------------------------------------------ Init: main5_3(emptyHeap, AddrRange(nthAddr(0), 0), 2) @@ -234,96 +236,18 @@ Init: | | V - main7_36_2(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(2), 1), 0) + main7_36_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(2), 1), 0) ------------------------------------------------------------------------------------------------------------------------ | | V - main7_36_2(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(0), 0), 1) + main7_36_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(0), 0), 1) ------------------------------------------------------------------------------------------------------------------------ Final: - main7_36_2(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(0), 0), 1) + main7_36_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 2)), AddrRange(nthAddr(1), 2), 2, AddrRange(nthAddr(0), 0), 1) ------------------------------------------------------------------------------------------------------------------------ Failed assertion: -false :- main7_36_2(@h, a:1, n:4, p:6, i:7), !is_O_Int(read(@h, nthAddrRange(p:6, 0))). (line:6 col:7) +false :- main7_36_3(@h, a:1, n:4, p:6, i:7), !is_O_Int(read(@h, nthAddrRange(p:6, 0))). (line:6 col:7) (property: valid-deref) - -global-struct-array-1.c -Warning: enabling heap model UNSAFE - ----------------------------------------------------------------------------------------------------------- -Init: - main8_3(newHeap(alloc(newHeap(alloc(emptyHeap, O_S(S(10)))), O_S(S(20)))), AddrRange(nthAddr(1), 2)) ----------------------------------------------------------------------------------------------------------- - | - | - V - main(newHeap(alloc(newHeap(alloc(emptyHeap, O_S(S(10)))), O_S(S(20)))), AddrRange(nthAddr(1), 2)) ----------------------------------------------------------------------------------------------------------- - | - | - V - main9_3(newHeap(alloc(newHeap(alloc(emptyHeap, O_S(S(10)))), O_S(S(20)))), AddrRange(nthAddr(1), 2), 20) ----------------------------------------------------------------------------------------------------------- - | - | - V - main_1(newHeap(alloc(newHeap(alloc(emptyHeap, O_S(S(10)))), O_S(S(21)))), AddrRange(nthAddr(1), 2)) ----------------------------------------------------------------------------------------------------------- -Final: - main_1(newHeap(alloc(newHeap(alloc(emptyHeap, O_S(S(10)))), O_S(S(21)))), AddrRange(nthAddr(1), 2)) ----------------------------------------------------------------------------------------------------------- -Failed assertion: -false :- main_1(@h, sArr:5), is_O_S(read(@h, nthAddrRange(sArr:5, 1))) & f(getS(read(@h, nthAddrRange(sArr:5, 1)))) != 1. (line:10 col:3) - - -array-of-ptr-1.c -Warning: enabling heap model -SAFE - -simple-dynamic-memsafety1.c -Warning: enabling heap model -SAFE -valid-memsafety/valid-memtrack - expected verdict matches the result! - -simple-dynamic-memsafety2.c -Warning: enabling heap model UNSAFE - ------------------------------------------------------------------------------------------ -Init: - main4_3(emptyHeap, AddrRange(nthAddr(0), 0)) ------------------------------------------------------------------------------------------ - | - | - V - main4_26_0(newBatchHeap(batchAlloc(emptyHeap, O_Int(11), 3)), AddrRange(nthAddr(1), 3)) ------------------------------------------------------------------------------------------ -Final: - main4_26_0(newBatchHeap(batchAlloc(emptyHeap, O_Int(11), 3)), AddrRange(nthAddr(1), 3)) ------------------------------------------------------------------------------------------ -Failed assertion: -false :- main4_26_0(@h, a:1), read(@h, __eval) != defObj. - -valid-memsafety/valid-memtrack - expected verdict matches the result! - -simple-global-memsafety1.c -Warning: enabling heap model -SAFE -valid-memsafety/valid-memtrack - expected verdict matches the result! - -simple-alloca-memsafety1.c -Warning: enabling heap model -SAFE -valid-memsafety/valid-memtrack - expected verdict matches the result! - -simple-alloca-memsafety2.c -Warning: enabling heap model -SAFE -valid-memsafety/valid-memtrack - expected verdict matches the result! diff --git a/regression-tests/horn-hcc-array/dynamic-loop1.c b/regression-tests/horn-hcc-array/dynamic-loop1.c index ec140ff..83577cb 100644 --- a/regression-tests/horn-hcc-array/dynamic-loop1.c +++ b/regression-tests/horn-hcc-array/dynamic-loop1.c @@ -21,4 +21,6 @@ void main() { } assert(sum == n*3); + + free(a); } diff --git a/regression-tests/horn-hcc-array/out-of-bounds-line1.yml b/regression-tests/horn-hcc-array/out-of-bounds-line1.yml index 385aa19..0b16430 100644 --- a/regression-tests/horn-hcc-array/out-of-bounds-line1.yml +++ b/regression-tests/horn-hcc-array/out-of-bounds-line1.yml @@ -5,6 +5,7 @@ input_files: 'out-of-bounds-line1.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: false + subproperty: valid-deref options: language: C diff --git a/regression-tests/horn-hcc-array/out-of-bounds-line2.yml b/regression-tests/horn-hcc-array/out-of-bounds-line2.yml index b8d1337..ef987ef 100644 --- a/regression-tests/horn-hcc-array/out-of-bounds-line2.yml +++ b/regression-tests/horn-hcc-array/out-of-bounds-line2.yml @@ -5,6 +5,7 @@ input_files: 'out-of-bounds-line2.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: false + subproperty: valid-deref options: language: C diff --git a/regression-tests/horn-hcc-array/out-of-bounds-line3.yml b/regression-tests/horn-hcc-array/out-of-bounds-line3.yml index 49474a8..bc35d5f 100644 --- a/regression-tests/horn-hcc-array/out-of-bounds-line3.yml +++ b/regression-tests/horn-hcc-array/out-of-bounds-line3.yml @@ -5,6 +5,7 @@ input_files: 'out-of-bounds-line3.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: false + subproperty: valid-deref options: language: C diff --git a/regression-tests/horn-hcc-array/out-of-bounds-line4.yml b/regression-tests/horn-hcc-array/out-of-bounds-line4.yml index fcc6950..ae1aec1 100644 --- a/regression-tests/horn-hcc-array/out-of-bounds-line4.yml +++ b/regression-tests/horn-hcc-array/out-of-bounds-line4.yml @@ -5,6 +5,7 @@ input_files: 'out-of-bounds-line4.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: false + subproperty: valid-deref options: language: C diff --git a/regression-tests/horn-hcc-array/out-of-bounds-loop.yml b/regression-tests/horn-hcc-array/out-of-bounds-loop.yml index f165871..b6cee4a 100644 --- a/regression-tests/horn-hcc-array/out-of-bounds-loop.yml +++ b/regression-tests/horn-hcc-array/out-of-bounds-loop.yml @@ -5,7 +5,7 @@ input_files: 'out-of-bounds-loop.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: false - subproperty: valid-memtrack + subproperty: valid-deref options: language: C diff --git a/regression-tests/horn-hcc-array/pointer-arith-1-safe.c b/regression-tests/horn-hcc-array/pointer-arith-1-safe.c index 7ee34c1..aa24c5f 100644 --- a/regression-tests/horn-hcc-array/pointer-arith-1-safe.c +++ b/regression-tests/horn-hcc-array/pointer-arith-1-safe.c @@ -8,4 +8,5 @@ void main() { assert(*p == 0); p = p+1; } + free(a); } diff --git a/regression-tests/horn-hcc-array/pointer-arith-1-safe.yml b/regression-tests/horn-hcc-array/pointer-arith-1-safe.yml new file mode 100644 index 0000000..f89087f --- /dev/null +++ b/regression-tests/horn-hcc-array/pointer-arith-1-safe.yml @@ -0,0 +1,13 @@ +format_version: '2.0' + +input_files: 'pointer-arith-1-safe.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: true + - property_file: ../properties/unreach-call.prp + expected_verdict: true + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/horn-hcc-array/pointer-arith-1-unsafe.c b/regression-tests/horn-hcc-array/pointer-arith-1-unsafe.c index d6683ae..9e4ddff 100644 --- a/regression-tests/horn-hcc-array/pointer-arith-1-unsafe.c +++ b/regression-tests/horn-hcc-array/pointer-arith-1-unsafe.c @@ -8,4 +8,5 @@ void main() { assert(*p == 0); p = p+1; } + free(a); } diff --git a/regression-tests/horn-hcc-array/pointer-arith-1-unsafe.yml b/regression-tests/horn-hcc-array/pointer-arith-1-unsafe.yml new file mode 100644 index 0000000..efea4da --- /dev/null +++ b/regression-tests/horn-hcc-array/pointer-arith-1-unsafe.yml @@ -0,0 +1,14 @@ +format_version: '2.0' + +input_files: 'pointer-arith-1-unsafe' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-deref + - property_file: ../properties/unreach-call.prp + expected_verdict: false + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/horn-hcc-array/pointer-arith-2-safe.c b/regression-tests/horn-hcc-array/pointer-arith-2-safe.c index cc6b97b..928f03d 100644 --- a/regression-tests/horn-hcc-array/pointer-arith-2-safe.c +++ b/regression-tests/horn-hcc-array/pointer-arith-2-safe.c @@ -8,4 +8,5 @@ void main() { assert(*p == 0); p += 1; } + free(a); } diff --git a/regression-tests/horn-hcc-array/pointer-arith-2-safe.yml b/regression-tests/horn-hcc-array/pointer-arith-2-safe.yml new file mode 100644 index 0000000..dd3e752 --- /dev/null +++ b/regression-tests/horn-hcc-array/pointer-arith-2-safe.yml @@ -0,0 +1,13 @@ +format_version: '2.0' + +input_files: 'pointer-arith-2-safe.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: true + - property_file: ../properties/unreach-call.prp + expected_verdict: true + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/horn-hcc-array/pointer-arith-2-unsafe.c b/regression-tests/horn-hcc-array/pointer-arith-2-unsafe.c index e60c804..ab0f7d5 100644 --- a/regression-tests/horn-hcc-array/pointer-arith-2-unsafe.c +++ b/regression-tests/horn-hcc-array/pointer-arith-2-unsafe.c @@ -8,4 +8,5 @@ void main() { assert(*p == 0); p += 1; } + free(a); } diff --git a/regression-tests/horn-hcc-array/pointer-arith-2-unsafe.yml b/regression-tests/horn-hcc-array/pointer-arith-2-unsafe.yml new file mode 100644 index 0000000..3acdc55 --- /dev/null +++ b/regression-tests/horn-hcc-array/pointer-arith-2-unsafe.yml @@ -0,0 +1,14 @@ +format_version: '2.0' + +input_files: 'pointer-arith-2-unsafe.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-deref + - property_file: ../properties/unreach-call.prp + expected_verdict: false + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/horn-hcc-array/pointer-arith-3-safe.c b/regression-tests/horn-hcc-array/pointer-arith-3-safe.c index 28fe124..e648899 100644 --- a/regression-tests/horn-hcc-array/pointer-arith-3-safe.c +++ b/regression-tests/horn-hcc-array/pointer-arith-3-safe.c @@ -8,4 +8,5 @@ void main() { assert(*p == 0); p = p+1; } + free(a); } diff --git a/regression-tests/horn-hcc-array/pointer-arith-3-safe.yml b/regression-tests/horn-hcc-array/pointer-arith-3-safe.yml new file mode 100644 index 0000000..86a2875 --- /dev/null +++ b/regression-tests/horn-hcc-array/pointer-arith-3-safe.yml @@ -0,0 +1,13 @@ +format_version: '2.0' + +input_files: 'pointer-arith-3-safe.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: true + - property_file: ../properties/unreach-call.prp + expected_verdict: true + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/horn-hcc-array/pointer-arith-3-unsafe.c b/regression-tests/horn-hcc-array/pointer-arith-3-unsafe.c index 656a28d..3aee527 100644 --- a/regression-tests/horn-hcc-array/pointer-arith-3-unsafe.c +++ b/regression-tests/horn-hcc-array/pointer-arith-3-unsafe.c @@ -5,7 +5,12 @@ void main() { a = calloc(sizeof(int)*n); int *p = &(a[1]); for(int i = 0; i < n; ++i) { - assert(*p == 0); + if(*p != 0) { + reach_error(); + } + // Above the read *p is unsafe (valid-deref), + // reach_error will also be hit (unreach-call), that location might not contain 0. p = p+1; } + free(a); } diff --git a/regression-tests/horn-hcc-array/pointer-arith-3-unsafe.yml b/regression-tests/horn-hcc-array/pointer-arith-3-unsafe.yml new file mode 100644 index 0000000..edde398 --- /dev/null +++ b/regression-tests/horn-hcc-array/pointer-arith-3-unsafe.yml @@ -0,0 +1,14 @@ +format_version: '2.0' + +input_files: 'pointer-arith-3-unsafe.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-deref + - property_file: ../properties/unreach-call.prp + expected_verdict: false + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/horn-hcc-array/runtests b/regression-tests/horn-hcc-array/runtests index 15a83b6..eb8b6b9 100755 --- a/regression-tests/horn-hcc-array/runtests +++ b/regression-tests/horn-hcc-array/runtests @@ -2,7 +2,7 @@ LAZABS=../../tri -TESTS="out-of-bounds-line1.c out-of-bounds-line2.c out-of-bounds-line3.c out-of-bounds-line4.c dynamic-loop1.c simple-dynamic-array.c simple-global-array.c array-single-alloc.c array-inside-struct-1.c pointer-arith-1-safe.c pointer-arith-1-unsafe.c pointer-arith-2-safe.c pointer-arith-2-unsafe.c pointer-arith-3-safe.c pointer-arith-3-unsafe.c global-struct-array-1.c array-of-ptr-1.c" +TESTS="out-of-bounds-line1.c out-of-bounds-line2.c out-of-bounds-line3.c out-of-bounds-line4.c dynamic-loop1.c simple-dynamic-array.c simple-global-array.c array-single-alloc.c array-inside-struct-1.c pointer-arith-1-safe.c pointer-arith-1-unsafe.c pointer-arith-2-safe.c pointer-arith-2-unsafe.c global-struct-array-1.c array-of-ptr-1.c" for name in $TESTS; do echo @@ -10,7 +10,7 @@ for name in $TESTS; do $LAZABS -cex -abstract:off "$@" $name 2>&1 | grep -v 'at ' done -MEMTRACKTESTS="simple-dynamic-memsafety1.c simple-dynamic-memsafety2.c simple-global-memsafety1.c simple-alloca-memsafety1.c simple-alloca-memsafety2.c" +MEMTRACKTESTS="simple-global-memsafety1.c simple-alloca-memsafety1.c simple-alloca-memsafety2.c" for name in $MEMTRACKTESTS; do echo @@ -18,3 +18,12 @@ for name in $MEMTRACKTESTS; do $LAZABS -cex -abstract:off "$@" $name 2>&1 | grep -v 'at ' # -memtrack can also be added but not required when .yml files are present done + +SPLITPROPERTYTESTS="pointer-arith-3-safe.c pointer-arith-3-unsafe.c" + +for name in $SPLITPROPERTYTESTS; do + echo + echo $name + $LAZABS -cex -abstract:off -splitProperties "$@" $name 2>&1 | grep -v 'at ' + # -memtrack can also be added but not required when .yml files are present +done diff --git a/regression-tests/horn-hcc-array/simple-alloca-memsafety1.yml b/regression-tests/horn-hcc-array/simple-alloca-memsafety1.yml index d50bcfa..1fe6356 100644 --- a/regression-tests/horn-hcc-array/simple-alloca-memsafety1.yml +++ b/regression-tests/horn-hcc-array/simple-alloca-memsafety1.yml @@ -5,7 +5,8 @@ input_files: 'simple-alloca-memsafety1.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: true - subproperty: valid-memtrack + - property_file: ../properties/valid-memcleanup.prp + expected_verdict: true options: language: C diff --git a/regression-tests/horn-hcc-array/simple-alloca-memsafety2.yml b/regression-tests/horn-hcc-array/simple-alloca-memsafety2.yml index d50bcfa..1fe6356 100644 --- a/regression-tests/horn-hcc-array/simple-alloca-memsafety2.yml +++ b/regression-tests/horn-hcc-array/simple-alloca-memsafety2.yml @@ -5,7 +5,8 @@ input_files: 'simple-alloca-memsafety1.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: true - subproperty: valid-memtrack + - property_file: ../properties/valid-memcleanup.prp + expected_verdict: true options: language: C diff --git a/regression-tests/horn-hcc-array/simple-dynamic-array.c b/regression-tests/horn-hcc-array/simple-dynamic-array.c index c4c199c..9135efe 100644 --- a/regression-tests/horn-hcc-array/simple-dynamic-array.c +++ b/regression-tests/horn-hcc-array/simple-dynamic-array.c @@ -5,4 +5,5 @@ void main() { a[0] = 1; a[1] = 2; assert((a[0] + a[1]) == 3); + free(a); } diff --git a/regression-tests/horn-hcc-array/simple-dynamic-memsafety1.c b/regression-tests/horn-hcc-array/simple-dynamic-memsafety1.c deleted file mode 100644 index ea2d0a2..0000000 --- a/regression-tests/horn-hcc-array/simple-dynamic-memsafety1.c +++ /dev/null @@ -1,6 +0,0 @@ -int a[]; - -void main() { - a = malloc(sizeof(int)*3); - free(a); -} diff --git a/regression-tests/horn-hcc-array/simple-dynamic-memsafety2.c b/regression-tests/horn-hcc-array/simple-dynamic-memsafety2.c deleted file mode 100644 index 642d556..0000000 --- a/regression-tests/horn-hcc-array/simple-dynamic-memsafety2.c +++ /dev/null @@ -1,5 +0,0 @@ -int a[]; - -void main() { - a = malloc(sizeof(int)*3); -} diff --git a/regression-tests/horn-hcc-array/simple-global-memsafety1.yml b/regression-tests/horn-hcc-array/simple-global-memsafety1.yml index 1fc7ad7..907bbc7 100644 --- a/regression-tests/horn-hcc-array/simple-global-memsafety1.yml +++ b/regression-tests/horn-hcc-array/simple-global-memsafety1.yml @@ -5,7 +5,8 @@ input_files: 'simple-global-memsafety1.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: true - subproperty: valid-memtrack + - property_file: ../properties/valid-memcleanup.prp + expected_verdict: true options: language: C diff --git a/regression-tests/horn-hcc-array/simple-stack-memsafety1.yml b/regression-tests/horn-hcc-array/simple-stack-memsafety1.yml index a08e8c5..8ef869f 100644 --- a/regression-tests/horn-hcc-array/simple-stack-memsafety1.yml +++ b/regression-tests/horn-hcc-array/simple-stack-memsafety1.yml @@ -5,7 +5,8 @@ input_files: 'simple-stack-memsafety1.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: true - subproperty: valid-memtrack + - property_file: ../properties/valid-memcleanup.prp + expected_verdict: true options: language: C diff --git a/regression-tests/horn-hcc-enum/Answers b/regression-tests/horn-hcc-enum/Answers index 36066ab..bc70a46 100644 --- a/regression-tests/horn-hcc-enum/Answers +++ b/regression-tests/horn-hcc-enum/Answers @@ -1,6 +1,5 @@ enum1.hcc -UNSAFE ------------ Init: @@ -10,11 +9,11 @@ Final: main9_3(3) ------------ Failed assertion: -false :- main9_3(x:8), x:8 != 0 & x:8 != 1 & x:8 != 2. (line:9 col:3) +false :- main9_3(x:8), x:8 != 0 & x:8 != 1 & x:8 != 2. (line:9 col:3) (property: user-assertion) +UNSAFE enum1-trailing-comma.hcc -UNSAFE ------------ Init: @@ -24,11 +23,11 @@ Final: main9_3(3) ------------ Failed assertion: -false :- main9_3(x:8), x:8 != 0 & x:8 != 1 & x:8 != 2. (line:9 col:3) +false :- main9_3(x:8), x:8 != 0 & x:8 != 1 & x:8 != 2. (line:9 col:3) (property: user-assertion) +UNSAFE enum2.hcc -UNSAFE ------------ Init: @@ -38,8 +37,9 @@ Final: main9_3(2) ------------ Failed assertion: -false :- main9_3(x:8), x:8 != 0 & x:8 != 1. (line:9 col:3) +false :- main9_3(x:8), x:8 != 0 & x:8 != 1. (line:9 col:3) (property: user-assertion) +UNSAFE enum3.hcc SAFE diff --git a/regression-tests/horn-hcc-heap/Answers b/regression-tests/horn-hcc-heap/Answers index 581e849..f5636ba 100644 --- a/regression-tests/horn-hcc-heap/Answers +++ b/regression-tests/horn-hcc-heap/Answers @@ -1,20 +1,12 @@ list-001.c -Warning: enabling heap model SAFE list-001-fail.c -Warning: enabling heap model -UNSAFE --------------------------------------------------------------------- Init: main11_3(emptyHeap) ---------------------------------------------------------------------- - | - | - V - main11_3_1(newHeap(alloc(emptyHeap, O_node(node(0)))), nthAddr(1)) --------------------------------------------------------------------- | | @@ -25,27 +17,16 @@ Final: main12_3(newHeap(alloc(emptyHeap, O_node(node(0)))), nthAddr(1), 0) --------------------------------------------------------------------- Failed assertion: -false :- main12_3(@h, list:11, y:12), y:12 = 0. (line:13 col:3) +false :- main12_3(@h, list:11, y:12), y:12 = 0. (line:13 col:3) (property: user-assertion) +UNSAFE list-002-fail.c -Warning: enabling heap model Warning: no definition of function "nondet_bool" available -UNSAFE ------------------------------------------------------------------------------------------------- Init: main14_3(emptyHeap) -------------------------------------------------------------------------------------------------- - | - | - V - main14_3_1(newHeap(alloc(emptyHeap, O_node(node(nthAddr(0), nthAddr(1))))), nthAddr(1)) -------------------------------------------------------------------------------------------------- - | - | - V - main(newHeap(alloc(emptyHeap, O_node(node(nthAddr(0), nthAddr(1))))), nthAddr(1)) ------------------------------------------------------------------------------------------------- | | @@ -56,320 +37,209 @@ Final: main_3(newHeap(alloc(emptyHeap, O_node(node(nthAddr(0), nthAddr(0))))), nthAddr(1), nthAddr(1)) ------------------------------------------------------------------------------------------------- Failed assertion: -false :- main_3(@h, list:14, tail:17), list:14 = tail:17. (line:29 col:3) +false :- main_3(@h, list:14, tail:17), list:14 = tail:17. (line:29 col:3) (property: user-assertion) +UNSAFE mutually-referential-structs.c -Warning: enabling heap model SAFE mutually-referential-structs-fail.c -Warning: enabling heap model SAFE mutually-referential-structs-unsafe.c -Warning: enabling heap model -UNSAFE ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ +--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Init: - main14_3(emptyHeap) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ - | - | - V - main15_3(newHeap(alloc(newHeap(alloc(emptyHeap, O_parent(parent(nthAddr(0), nthAddr(0))))), O_child(child(nthAddr(0))))), nthAddr(1), nthAddr(2)) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ - | - | - V - main(newHeap(alloc(newHeap(alloc(emptyHeap, O_parent(parent(nthAddr(2), nthAddr(0))))), O_child(child(nthAddr(0))))), nthAddr(1)) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ - | - | - V - main17_3(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_parent(parent(nthAddr(2), nthAddr(0))))), O_child(child(nthAddr(1))))), O_child(child(nthAddr(0))))), nthAddr(1), nthAddr(3)) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ - | - | - V - main_3(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_parent(parent(nthAddr(2), nthAddr(3))))), O_child(child(nthAddr(1))))), O_child(child(nthAddr(0))))), nthAddr(1)) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ + main14_3(emptyHeap) +--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + main_3(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_parent(parent(nthAddr(2), nthAddr(3))))), O_child(child(nthAddr(1))))), O_child(child(nthAddr(0))))), nthAddr(1)) +--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Final: - main_3(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_parent(parent(nthAddr(2), nthAddr(3))))), O_child(child(nthAddr(1))))), O_child(child(nthAddr(0))))), nthAddr(1)) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ + main_3(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_parent(parent(nthAddr(2), nthAddr(3))))), O_child(child(nthAddr(1))))), O_child(child(nthAddr(0))))), nthAddr(1)) +--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Failed assertion: -false :- main_3(@h, list:14), is_O_parent(read(@h, list:14)) & is_O_child(read(@h, child1(getparent(read(@h, list:14))))) & is_O_parent(read(@h, list:14)) & is_O_child(read(@h, child2(getparent(read(@h, list:14))))) & p(getchild(read(@h, child1(getparent(read(@h, list:14)))))) != p(getchild(read(@h, child2(getparent(read(@h, list:14)))))). (line:20 col:3) +false :- main_3(@h, list:14), p(getchild(read(@h, child1(getparent(read(@h, list:14)))))) != p(getchild(read(@h, child2(getparent(read(@h, list:14)))))). (line:20 col:3) (property: user-assertion) +UNSAFE simple-struct.c -Warning: enabling heap model SAFE simple-struct-2.c -Warning: enabling heap model SAFE simple-struct-fail.c -Warning: enabling heap model SAFE swap-1.c -Warning: enabling heap model SAFE swap-1-fail.c -Warning: enabling heap model SAFE swap-2.c -Warning: enabling heap model SAFE swap-2-fail.c -Warning: enabling heap model SAFE swap-3.c -Warning: enabling heap model SAFE simple-arith.c -Warning: enabling heap model SAFE typecastUnsafe-001.c -Warning: enabling heap model -UNSAFE ----------------------------------------------------------------------- +---------------------------------------------------------------------------------- Init: - main6_3(emptyHeap) ----------------------------------------------------------------------- - | - | - V - main7_3(newHeap(alloc(emptyHeap, O_Int(0))), nthAddr(1), nthAddr(1)) ----------------------------------------------------------------------- + main6_3(emptyHeap, nthAddr(0)) +---------------------------------------------------------------------------------- + | + | + V + main7_3(newHeap(alloc(emptyHeap, O_Int(0))), nthAddr(0), nthAddr(1), nthAddr(1)) +---------------------------------------------------------------------------------- Final: - main7_3(newHeap(alloc(emptyHeap, O_Int(0))), nthAddr(1), nthAddr(1)) ----------------------------------------------------------------------- + main7_3(newHeap(alloc(emptyHeap, O_Int(0))), nthAddr(0), nthAddr(1), nthAddr(1)) +---------------------------------------------------------------------------------- Failed assertion: -false :- main7_3(@h, x:6, y:7), !is_O_S(read(@h, y:7)). (line:7 col:12) +false :- main7_3(@h, @v_cleanup, x:6, y:7), !is_O_S(read(@h, y:7)). (line:7 col:12) (property: valid-deref) +UNSAFE typecastSafe-001.c -Warning: enabling heap model SAFE illegal-access-001.c -Warning: enabling heap model tricera.concurrency.ccreader.CCExceptions$TranslationException: Pointer arithmetic is not allowed, and the only possible initialization value for pointers is 0 (NULL) (error "Pointer arithmetic is not allowed, and the only possible initialization value for pointers is 0 (NULL)") Other Error: Pointer arithmetic is not allowed, and the only possible initialization value for pointers is 0 (NULL) illegal-access-002.c -Warning: enabling heap model tricera.concurrency.ccreader.CCExceptions$TranslationException: Pointer arithmetic is not allowed, and the only assignable integer value for pointers is 0 (NULL) (error "Pointer arithmetic is not allowed, and the only assignable integer value for pointers is 0 (NULL)") Other Error: Pointer arithmetic is not allowed, and the only assignable integer value for pointers is 0 (NULL) postop.c -Warning: enabling heap model SAFE postop-struct.c -Warning: enabling heap model SAFE preop.c -Warning: enabling heap model SAFE preop-struct.c -Warning: enabling heap model SAFE opassign.c -Warning: enabling heap model SAFE opassign-struct.c -Warning: enabling heap model SAFE unsafe-access-001.c -Warning: enabling heap model -UNSAFE ----------------------------------------------------------------------- +---------------------------------------------------------------------------------- Init: - main2_3(emptyHeap) ----------------------------------------------------------------------- - | - | - V - main3_3(newHeap(alloc(emptyHeap, O_Int(0))), nthAddr(1), nthAddr(0)) ----------------------------------------------------------------------- + main2_3(emptyHeap, nthAddr(0)) +---------------------------------------------------------------------------------- + | + | + V + main3_3(newHeap(alloc(emptyHeap, O_Int(0))), nthAddr(0), nthAddr(1), nthAddr(0)) +---------------------------------------------------------------------------------- Final: - main3_3(newHeap(alloc(emptyHeap, O_Int(0))), nthAddr(1), nthAddr(0)) ----------------------------------------------------------------------- + main3_3(newHeap(alloc(emptyHeap, O_Int(0))), nthAddr(0), nthAddr(1), nthAddr(0)) +---------------------------------------------------------------------------------- Failed assertion: -false :- main3_3(@h, x:2, y:3), !is_O_Addr(read(@h, y:3)). (line:3 col:7) +false :- main3_3(@h, @v_cleanup, x:2, y:3), !is_O_Addr(read(@h, y:3)). (line:3 col:7) (property: valid-deref) +UNSAFE stackptr-to-heapptr.c -Warning: enabling heap model SAFE free-1-unsafe.c -Warning: enabling heap model -UNSAFE ------------------------------------------------------ +------------------------------------------------------------------------ Init: - main2_3(emptyHeap) ------------------------------------------------------ - | - | - V - main(newHeap(alloc(emptyHeap, defObj)), nthAddr(1)) ------------------------------------------------------ + main2_3(emptyHeap, nthAddr(0)) +------------------------------------------------------------------------ + | + | + V + main2_3_1(newHeap(alloc(emptyHeap, O_Int(9))), nthAddr(0), nthAddr(1)) +------------------------------------------------------------------------ + | + | + V + main(newHeap(alloc(emptyHeap, defObj)), nthAddr(0), nthAddr(1)) +------------------------------------------------------------------------ Final: - main(newHeap(alloc(emptyHeap, defObj)), nthAddr(1)) ------------------------------------------------------ + main(newHeap(alloc(emptyHeap, defObj)), nthAddr(0), nthAddr(1)) +------------------------------------------------------------------------ Failed assertion: -false :- main(@h, a:2), !is_O_Int(read(@h, a:2)). (line:2 col:7) +false :- main(@h, @v_cleanup, a:2), !is_O_Int(read(@h, a:2)). (line:2 col:7) (property: valid-deref) +UNSAFE free-2-nondet-unsafe.c -Warning: enabling heap model Warning: no definition of function "nondet" available -UNSAFE ------------------------------------------------------ +------------------------------------------------------------------------ Init: - main4_3(emptyHeap) ------------------------------------------------------ - | - | - V - main(newHeap(alloc(emptyHeap, defObj)), nthAddr(1)) ------------------------------------------------------ + main4_3(emptyHeap, nthAddr(0)) +------------------------------------------------------------------------ + | + | + V + main5_6_2(newHeap(alloc(emptyHeap, O_Int(9))), nthAddr(0), nthAddr(1)) +------------------------------------------------------------------------ + | + | + V + main(newHeap(alloc(emptyHeap, defObj)), nthAddr(0), nthAddr(1)) +------------------------------------------------------------------------ Final: - main(newHeap(alloc(emptyHeap, defObj)), nthAddr(1)) ------------------------------------------------------ + main(newHeap(alloc(emptyHeap, defObj)), nthAddr(0), nthAddr(1)) +------------------------------------------------------------------------ Failed assertion: -false :- main(@h, a:4), !is_O_Int(read(@h, a:4)). (line:4 col:7) +false :- main(@h, @v_cleanup, a:4), !is_O_Int(read(@h, a:4)). (line:4 col:7) (property: valid-deref) +UNSAFE free-3-safe.c -Warning: enabling heap model SAFE free-4-unsafe.c -Warning: enabling heap model -UNSAFE --------------------------------------------------------------------- +-------------------------------------------------------------------------------- Init: - main4_3(emptyHeap) --------------------------------------------------------------------- - | - | - V - main6_3(newHeap(alloc(emptyHeap, defObj)), nthAddr(1), nthAddr(1)) --------------------------------------------------------------------- + main4_3(emptyHeap, nthAddr(0)) +-------------------------------------------------------------------------------- + | + | + V + main4_3_1(newHeap(alloc(emptyHeap, O_Int(9))), nthAddr(0), nthAddr(1)) +-------------------------------------------------------------------------------- + | + | + V + main6_3(newHeap(alloc(emptyHeap, defObj)), nthAddr(0), nthAddr(1), nthAddr(1)) +-------------------------------------------------------------------------------- Final: - main6_3(newHeap(alloc(emptyHeap, defObj)), nthAddr(1), nthAddr(1)) --------------------------------------------------------------------- + main6_3(newHeap(alloc(emptyHeap, defObj)), nthAddr(0), nthAddr(1), nthAddr(1)) +-------------------------------------------------------------------------------- Failed assertion: -false :- main6_3(@h, a:4, b:6), !is_O_Int(read(@h, b:6)). (line:6 col:7) - +false :- main6_3(@h, @v_cleanup, a:4, b:6), !is_O_Int(read(@h, b:6)). (line:6 col:7) (property: valid-deref) -struct-ptrfield-1.c -Warning: enabling heap model -SAFE - -memtrack-01.c -Warning: enabling heap model -UNSAFE - ------------------------------------------------- -Init: - main2_3_1(emptyHeap) ------------------------------------------------- - | - | - V - main2_3_0(newHeap(alloc(emptyHeap, O_Int(9)))) ------------------------------------------------- -Final: - main2_3_0(newHeap(alloc(emptyHeap, O_Int(9)))) ------------------------------------------------- -Failed assertion: -false :- main2_3_0(@h), read(@h, __eval) != defObj. - -valid-memsafety/valid-memtrack - expected verdict matches the result! - -memtrack-02.c -Warning: enabling heap model -SAFE -valid-memsafety/valid-memtrack - expected verdict matches the result! - -memtrack-03.c -Warning: enabling heap model UNSAFE --------------------------------------------------- -Init: - main6_3(emptyHeap) --------------------------------------------------- - | - | - V - main7_10(newHeap(alloc(emptyHeap, O_Int(9))), 0) --------------------------------------------------- -Final: - main7_10(newHeap(alloc(emptyHeap, O_Int(9))), 0) --------------------------------------------------- -Failed assertion: -false :- main7_10(@h, _res2), read(@h, __eval) != defObj. - -valid-memsafety/valid-memtrack - expected verdict matches the result! - -memtrack-04.c -SAFE -valid-memsafety/valid-memtrack - expected verdict matches the result! - -memtrack-05.c -Warning: enabling heap model -UNSAFE - --------------------------------------------------- -Init: - main7_3(emptyHeap, nthAddr(0)) --------------------------------------------------- - | - | - V - main8_10(newHeap(alloc(emptyHeap, O_Int(9))), 0) --------------------------------------------------- -Final: - main8_10(newHeap(alloc(emptyHeap, O_Int(9))), 0) --------------------------------------------------- -Failed assertion: -false :- main8_10(@h, _res2), read(@h, __eval) != defObj. - -valid-memsafety/valid-memtrack - expected verdict matches the result! - -memtrack-06.c -Warning: enabling heap model +struct-ptrfield-1.c SAFE -valid-memsafety/valid-memtrack - expected verdict matches the result! diff --git a/regression-tests/horn-hcc-heap/memtrack-03.yml b/regression-tests/horn-hcc-heap/free-1-unsafe.yml similarity index 72% rename from regression-tests/horn-hcc-heap/memtrack-03.yml rename to regression-tests/horn-hcc-heap/free-1-unsafe.yml index a2cfb9f..66a9d66 100644 --- a/regression-tests/horn-hcc-heap/memtrack-03.yml +++ b/regression-tests/horn-hcc-heap/free-1-unsafe.yml @@ -1,11 +1,11 @@ format_version: '2.0' -input_files: 'memtrack-03.c' +input_files: 'free-1-unsafe.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: false - subproperty: valid-memtrack + subproperty: valid-deref options: language: C diff --git a/regression-tests/horn-hcc-array/simple-dynamic-memsafety2.yml b/regression-tests/horn-hcc-heap/free-2-nondet-unsafe.yml similarity index 68% rename from regression-tests/horn-hcc-array/simple-dynamic-memsafety2.yml rename to regression-tests/horn-hcc-heap/free-2-nondet-unsafe.yml index 97db728..222d31c 100644 --- a/regression-tests/horn-hcc-array/simple-dynamic-memsafety2.yml +++ b/regression-tests/horn-hcc-heap/free-2-nondet-unsafe.yml @@ -1,11 +1,11 @@ format_version: '2.0' -input_files: 'simple-dynamic-memsafety2.c' +input_files: 'free-2-nondet-unsafe.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: false - subproperty: valid-memtrack + subproperty: valid-deref options: language: C diff --git a/regression-tests/horn-hcc-heap/memtrack-06.yml b/regression-tests/horn-hcc-heap/free-3-safe.yml similarity index 72% rename from regression-tests/horn-hcc-heap/memtrack-06.yml rename to regression-tests/horn-hcc-heap/free-3-safe.yml index 8cf73e5..9021036 100644 --- a/regression-tests/horn-hcc-heap/memtrack-06.yml +++ b/regression-tests/horn-hcc-heap/free-3-safe.yml @@ -1,11 +1,10 @@ format_version: '2.0' -input_files: 'memtrack-06.c' +input_files: 'free-3-safe.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: true - subproperty: valid-memtrack options: language: C diff --git a/regression-tests/horn-hcc-heap/memtrack-01.yml b/regression-tests/horn-hcc-heap/free-4-unsafe.yml similarity index 72% rename from regression-tests/horn-hcc-heap/memtrack-01.yml rename to regression-tests/horn-hcc-heap/free-4-unsafe.yml index 6296acf..d7acac2 100644 --- a/regression-tests/horn-hcc-heap/memtrack-01.yml +++ b/regression-tests/horn-hcc-heap/free-4-unsafe.yml @@ -1,11 +1,11 @@ format_version: '2.0' -input_files: 'memtrack-01.c' +input_files: 'free-4-unsafe.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: false - subproperty: valid-memtrack + subproperty: valid-deref options: language: C diff --git a/regression-tests/horn-hcc-heap/memtrack-01.c b/regression-tests/horn-hcc-heap/memtrack-01.c deleted file mode 100644 index da1cde4..0000000 --- a/regression-tests/horn-hcc-heap/memtrack-01.c +++ /dev/null @@ -1,3 +0,0 @@ -void main() { - int *x = malloc(sizeof *x); -} diff --git a/regression-tests/horn-hcc-heap/memtrack-03.c b/regression-tests/horn-hcc-heap/memtrack-03.c deleted file mode 100644 index 1af9dce..0000000 --- a/regression-tests/horn-hcc-heap/memtrack-03.c +++ /dev/null @@ -1,8 +0,0 @@ -void foo() { - malloc(sizeof(int)); -} - -int main() { - foo(); - return 0; -} diff --git a/regression-tests/horn-hcc-heap/memtrack-04.c b/regression-tests/horn-hcc-heap/memtrack-04.c deleted file mode 100644 index ca7f583..0000000 --- a/regression-tests/horn-hcc-heap/memtrack-04.c +++ /dev/null @@ -1,7 +0,0 @@ -void foo() { - malloc(sizeof(int)); -} - -int main() { - return 0; -} diff --git a/regression-tests/horn-hcc-heap/memtrack-05.c b/regression-tests/horn-hcc-heap/memtrack-05.c deleted file mode 100644 index 0992e74..0000000 --- a/regression-tests/horn-hcc-heap/memtrack-05.c +++ /dev/null @@ -1,9 +0,0 @@ -void foo(int **x) { - *x = malloc(sizeof(int)); -} - -int main() { - int *x; - foo(&x); - return 0; // unsafe -} diff --git a/regression-tests/horn-hcc-heap/memtrack-06.c b/regression-tests/horn-hcc-heap/memtrack-06.c deleted file mode 100644 index 0b4e48d..0000000 --- a/regression-tests/horn-hcc-heap/memtrack-06.c +++ /dev/null @@ -1,10 +0,0 @@ -void foo(int **x) { - *x = malloc(sizeof(int)); -} - -int main() { - int *x; - foo(&x); - free(x); - return 0; // safe -} diff --git a/regression-tests/horn-hcc-heap/runtests b/regression-tests/horn-hcc-heap/runtests index 3a02d00..2096c67 100755 --- a/regression-tests/horn-hcc-heap/runtests +++ b/regression-tests/horn-hcc-heap/runtests @@ -10,15 +10,6 @@ for name in $TESTS; do $LAZABS -cex -abstract:off "$@" $name 2>&1 | grep -v 'at ' done -MEMTRACKTESTS="memtrack-01.c memtrack-02.c memtrack-03.c memtrack-04.c memtrack-05.c memtrack-06.c " - -for name in $MEMTRACKTESTS; do - echo - echo $name - $LAZABS -cex -abstract:off "$@" $name 2>&1 | grep -v 'at ' - # -memtrack can also be added but not required when .yml files are present -done - # this one runs forever with the current encoding #TESTS="list-002.c" diff --git a/regression-tests/horn-hcc-heap/struct-ptrfield-1.c b/regression-tests/horn-hcc-heap/struct-ptrfield-1.c index 226b237..ad4e7df 100644 --- a/regression-tests/horn-hcc-heap/struct-ptrfield-1.c +++ b/regression-tests/horn-hcc-heap/struct-ptrfield-1.c @@ -10,5 +10,6 @@ void alloc(struct S *ps) { int main() { struct S s; alloc(&s); + free(s.f); return 0; } diff --git a/regression-tests/horn-hcc-heap/memtrack-02.yml b/regression-tests/horn-hcc-heap/struct-ptrfield-1.yml similarity index 85% rename from regression-tests/horn-hcc-heap/memtrack-02.yml rename to regression-tests/horn-hcc-heap/struct-ptrfield-1.yml index 00dc1d7..1f24065 100644 --- a/regression-tests/horn-hcc-heap/memtrack-02.yml +++ b/regression-tests/horn-hcc-heap/struct-ptrfield-1.yml @@ -5,7 +5,6 @@ input_files: 'memtrack-02.c' properties: - property_file: ../properties/valid-memsafety.prp expected_verdict: true - subproperty: valid-memtrack options: language: C diff --git a/regression-tests/horn-hcc-heap/typecastSafe-001.c b/regression-tests/horn-hcc-heap/typecastSafe-001.c index c70a848..e3dad00 100644 --- a/regression-tests/horn-hcc-heap/typecastSafe-001.c +++ b/regression-tests/horn-hcc-heap/typecastSafe-001.c @@ -10,5 +10,6 @@ void main() { *x = 42; assert(*z == *x); assert(*z == 42); + free(y); } diff --git a/regression-tests/horn-hcc-array/simple-global-array.yml b/regression-tests/horn-hcc-heap/typecastSafe-001.yml similarity index 86% rename from regression-tests/horn-hcc-array/simple-global-array.yml rename to regression-tests/horn-hcc-heap/typecastSafe-001.yml index adcb248..1d62cc7 100644 --- a/regression-tests/horn-hcc-array/simple-global-array.yml +++ b/regression-tests/horn-hcc-heap/typecastSafe-001.yml @@ -1,12 +1,12 @@ format_version: '2.0' -input_files: 'simple-global-array.c' +input_files: 'typecastSafe-001.c' properties: - - property_file: ../properties/valid-memsafety.prp - expected_verdict: true - property_file: ../properties/unreach-call.prp expected_verdict: true + - property_file: ../properties/valid-memsafety.prp + expected_verdict: true options: language: C diff --git a/regression-tests/horn-hcc-heap/typecastUnsafe-001.yml b/regression-tests/horn-hcc-heap/typecastUnsafe-001.yml new file mode 100644 index 0000000..af076be --- /dev/null +++ b/regression-tests/horn-hcc-heap/typecastUnsafe-001.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'typecastUnsafe-001.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-deref + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/horn-hcc-heap/unsafe-access-001.yml b/regression-tests/horn-hcc-heap/unsafe-access-001.yml new file mode 100644 index 0000000..8ab7052 --- /dev/null +++ b/regression-tests/horn-hcc-heap/unsafe-access-001.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'unsafe-access-001.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-deref + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/horn-hcc-pointer/Answers b/regression-tests/horn-hcc-pointer/Answers index 7321179..16c33e6 100644 --- a/regression-tests/horn-hcc-pointer/Answers +++ b/regression-tests/horn-hcc-pointer/Answers @@ -6,7 +6,6 @@ fields.hcc SAFE fields-nested.hcc -UNSAFE ----------------------------------------------------------------- Init: @@ -26,8 +25,9 @@ Final: main_4(.AS0(1, .AS1(5, .AS2(6))), .AS0(4, .AS1(2, .AS2(3))), 0) ----------------------------------------------------------------- Failed assertion: -false :- main_4(s1:9, s2:9, x1:21), a(b(s1:9)) != a(b(s1:9)) | a(b(s1:9)) != 2 | a(b(s2:9)) != 5. (line:23 col:5) +false :- main_4(s1:9, s2:9, x1:21), a(b(s1:9)) != a(b(s1:9)) | a(b(s1:9)) != 2 | a(b(s2:9)) != 5. (line:23 col:5) (property: user-assertion) +UNSAFE struct-pointer.hcc SAFE @@ -52,9 +52,7 @@ cast-stack-heap-01.c SAFE ptrptr-bug-1.c -Warning: enabling heap model SAFE ptrptr-bug-2.c -Warning: enabling heap model SAFE diff --git a/regression-tests/horn-hcc/Answers b/regression-tests/horn-hcc/Answers index da86866..a30185f 100644 --- a/regression-tests/horn-hcc/Answers +++ b/regression-tests/horn-hcc/Answers @@ -53,7 +53,6 @@ inits2.hcc SAFE inits3.hcc -UNSAFE --------------- Init: @@ -68,8 +67,9 @@ Final: main(1, 0) --------------- Failed assertion: -false :- main(g:3, h:4), g:3 != 0. (line:8 col:3) +false :- main(g:3, h:4), g:3 != 0. (line:8 col:3) (property: user-assertion) +UNSAFE shadowing.hcc SAFE @@ -120,7 +120,6 @@ down_true-unreach-call.i.c SAFE ternary-bug.c -UNSAFE --------------- Init: @@ -135,8 +134,9 @@ Final: main(1, 0, 0) --------------- Failed assertion: -false :- main(x:2, y:2, z:3). (line:5 col:3) +false :- main(x:2, y:2, z:3). (line:5 col:3) (property: user-assertion) +UNSAFE assert-ite-1.c SAFE @@ -145,7 +145,6 @@ assert-ite-2.c SAFE function-in-assume-assert-1-false.c -UNSAFE ------------------ Init: @@ -160,14 +159,14 @@ Final: main5_1(0, 1, 1) ------------------ Failed assertion: -false :- main5_1(x:10, y:11, __eval5_7:5), __eval5_7:5 != 0. (line:13 col:3) +false :- main5_1(x:10, y:11, __eval5_7:5), __eval5_7:5 != 0. (line:13 col:3) (property: user-assertion) +UNSAFE function-in-assume-assert-1-true.c SAFE function-in-assume-assert-2-false.c -UNSAFE ----------------------- Init: @@ -182,14 +181,14 @@ Final: main13_16(2, 1, 2, 1) ----------------------- Failed assertion: -false :- main13_16(x:10, y:11, __eval10_13:10, ite_13_16:1), __eval10_13:10 != ite_13_16:1. (line:13 col:3) +false :- main13_16(x:10, y:11, __eval10_13:10, ite_13_16:1), __eval10_13:10 != ite_13_16:1. (line:13 col:3) (property: user-assertion) +UNSAFE function-in-assume-assert-2-true.c SAFE function-in-assume-assert-3-false.c -UNSAFE ----------------------- Init: @@ -204,8 +203,9 @@ Final: main15_16(2, 1, 2, 1) ----------------------- Failed assertion: -false :- main15_16(x:12, y:13, __eval12_15:12, ite_15_16:1), __eval12_15:12 != ite_15_16:1. (line:15 col:3) +false :- main15_16(x:12, y:13, __eval12_15:12, ite_15_16:1), __eval12_15:12 != ite_15_16:1. (line:15 col:3) (property: user-assertion) +UNSAFE function-in-assume-assert-3-true.c SAFE diff --git a/regression-tests/horn-hcc/diamond_true-unreach-call1.c b/regression-tests/horn-hcc/diamond_true-unreach-call1.c index 62e31c0..2b5353c 100644 --- a/regression-tests/horn-hcc/diamond_true-unreach-call1.c +++ b/regression-tests/horn-hcc/diamond_true-unreach-call1.c @@ -9,5 +9,5 @@ int main(void) { x++; } } - __VERIFIER_assert((x % 2) == (y % 2)); + assert((x % 2) == (y % 2)); } diff --git a/regression-tests/horn-hcc/down_true-unreach-call.i.c b/regression-tests/horn-hcc/down_true-unreach-call.i.c index 511fa53..91e57f9 100644 --- a/regression-tests/horn-hcc/down_true-unreach-call.i.c +++ b/regression-tests/horn-hcc/down_true-unreach-call.i.c @@ -2,7 +2,7 @@ extern void __VERIFIER_error(void); extern void __VERIFIER_assume(int); void __VERIFIER_assert(int cond) { if (!(cond)) { - ERROR: __VERIFIER_error(); + ERROR: reach_error(); } return; } diff --git a/regression-tests/interpreted-predicates/Answers b/regression-tests/interpreted-predicates/Answers index ccdab57..d6b3123 100644 --- a/regression-tests/interpreted-predicates/Answers +++ b/regression-tests/interpreted-predicates/Answers @@ -1,6 +1,5 @@ simple-invariant-false.c -UNSAFE ------------ Init: @@ -15,14 +14,14 @@ Final: main(3) ------------ Failed assertion: -false :- main(x:8), x:8 != 42. (line:10 col:3) +false :- main(x:8), x:8 != 42. (line:10 col:3) (property: user-assertion) +UNSAFE simple-invariant-true.c SAFE simple-invariant-false.c -UNSAFE ------------ Init: @@ -37,8 +36,9 @@ Final: main(3) ------------ Failed assertion: -false :- main(x:8), x:8 != 42. (line:10 col:3) +false :- main(x:8), x:8 != 42. (line:10 col:3) (property: user-assertion) +UNSAFE simple-loop-invariant-true.c SAFE diff --git a/regression-tests/math-arrays/Answers b/regression-tests/math-arrays/Answers index a769d30..a99d572 100644 --- a/regression-tests/math-arrays/Answers +++ b/regression-tests/math-arrays/Answers @@ -1,11 +1,11 @@ simple-math-array-1.hcc -SAFE Solution (Prolog) ================================================================================ -main10_7_3(a:4,n:5,i:6) :- ((n:5 = 3), ((((i:6 = 2), (select(a:4, 2) = 2)); (((i:6 =< 2), (i:6 >= 1)), ((select(a:4, (1 + i:6)) = (1 + i:6)), (select(a:4, i:6) = i:6)))); (((i:6 =< 2), (i:6 >= 0)), (((select(a:4, (2 + i:6)) = (2 + i:6)), (select(a:4, (1 + i:6)) = (1 + i:6))), (select(a:4, i:6) = i:6))))). -main7_3(a:4,n:5,i:6) :- ((i:6 = 0), (n:5 = 3)). -main7_7(a:4,n:5,i:6) :- ((n:5 = 3), ((i:6 = 0); (((i:6 = 1), (select(a:4, 0) = 0)); ((((i:6 =< 3), (i:6 >= 1)), ((select(a:4, 1) = 1), (select(a:4, 0) = 0))), (\+((i:6 = 3)); (select(a:4, 2) = 2)))))). +main10_7_3(a:4, n:5, i:6) :- n:5 = 3 & ((i:6 = 2 & select(a:4, 2) = 2) | (2 >= i:6 & i:6 >= 1 & select(a:4, 1 + i:6) = 1 + i:6 & select(a:4, i:6) = i:6) | (2 >= i:6 & i:6 >= 0 & select(a:4, 2 + i:6) = 2 + i:6 & select(a:4, 1 + i:6) = 1 + i:6 & select(a:4, i:6) = i:6)). +main7_3(a:4, n:5, i:6) :- i:6 = 0 & n:5 = 3. +main7_7(a:4, n:5, i:6) :- n:5 = 3 & (i:6 = 0 | (i:6 = 1 & select(a:4, 0) = 0) | (3 >= i:6 & i:6 >= 1 & select(a:4, 1) = 1 & select(a:4, 0) = 0 & (i:6 != 3 | select(a:4, 2) = 2))). ================================================================================ +SAFE diff --git a/regression-tests/properties/Answers b/regression-tests/properties/Answers new file mode 100644 index 0000000..31199bf --- /dev/null +++ b/regression-tests/properties/Answers @@ -0,0 +1,73 @@ + +valid-free-10-true.c +SAFE + +valid-free-3-true.c +SAFE + +valid-free-7-false.c +UNSAFE + +valid-free-11-true.c +SAFE + +valid-free-4-false.c +UNSAFE + +valid-free-8-false.c +UNSAFE + +valid-free-1-true.c +SAFE + +valid-free-5-false.c +UNSAFE + +valid-free-9-false.c +UNSAFE + +valid-free-2-false.c +UNSAFE + +valid-free-6-true.c +SAFE + +valid-deref-arraybounds-1-false.c +UNSAFE + +valid-deref-arraybounds-3-true.c +Warning: no definition of function "nondet" available +Warning: no definition of function "nondet" available +SAFE + +valid-deref-arraybounds-2-false.c +UNSAFE + +valid-deref-nullptr-false.c +UNSAFE + +valid-deref-arraybounds-3-false.c +Warning: no definition of function "nondet" available +Warning: no definition of function "nondet" available +UNSAFE + +valid-deref-uninit-false.c +UNSAFE + +valid-deref-arraybounds-4-false.c +UNSAFE + +valid-memcleanup-1-false.c +UNSAFE + +valid-memcleanup-array-false.c +UNSAFE + +valid-memcleanup-1-true.c +SAFE + +valid-memcleanup-array-true.c +SAFE + +valid-memtrack-array-true.c +UNKNOWN (memcleanup violated - memtrack inconclusive) diff --git a/regression-tests/properties/runtests b/regression-tests/properties/runtests new file mode 100755 index 0000000..5149263 --- /dev/null +++ b/regression-tests/properties/runtests @@ -0,0 +1,21 @@ +#!/bin/sh + +LAZABS=../../tri + +TESTS="valid-free-10-true.c valid-free-3-true.c valid-free-7-false.c \ + valid-free-11-true.c valid-free-4-false.c valid-free-8-false.c \ + valid-free-1-true.c valid-free-5-false.c valid-free-9-false.c \ + valid-free-2-false.c valid-free-6-true.c \ + valid-deref-arraybounds-1-false.c valid-deref-arraybounds-3-true.c \ + valid-deref-arraybounds-2-false.c valid-deref-nullptr-false.c \ + valid-deref-arraybounds-3-false.c valid-deref-uninit-false.c \ + valid-deref-arraybounds-4-false.c \ + valid-memcleanup-1-false.c valid-memcleanup-array-false.c \ + valid-memcleanup-1-true.c valid-memcleanup-array-true.c \ + valid-memtrack-array-true.c" + +for name in $TESTS; do + echo + echo $name + $LAZABS -abstract:off "$@" $name 2>&1 | grep -v 'at ' +done diff --git a/regression-tests/properties/todo/README.md b/regression-tests/properties/todo/README.md new file mode 100644 index 0000000..d51e7e2 --- /dev/null +++ b/regression-tests/properties/todo/README.md @@ -0,0 +1,7 @@ +Stack pointers in functions are currently not fully supported by TriCera, and the stack pointer tests as a result do not currently work - both true and false versions will return "UNSAFE", as they are modelled (incorrectly) using the theory of heaps. + +valid-deref-type-1-false.c +No distinction is made between int and long in default settings, and it seems this also does not work using machine integer semantics. This should be fixed. + +valid-deref-type-2-false.c and valid-deref-type-2-true.c +No distinction is made between int and long in default settings, and it seems this also does not work using machine integer semantics (throws an error). This should be fixed. \ No newline at end of file diff --git a/regression-tests/properties/todo/valid-deref-stack-1-false.c b/regression-tests/properties/todo/valid-deref-stack-1-false.c new file mode 100644 index 0000000..d17ec82 --- /dev/null +++ b/regression-tests/properties/todo/valid-deref-stack-1-false.c @@ -0,0 +1,9 @@ +int* invalidStackAccess() { + int a = 10; // Local variable + return &a; // Returning address of local variable - leads to invalid access +} + +void main() { + int *p = invalidStackAccess(); + *p = 20; // Invalid access, dereferencing a dangling pointer +} diff --git a/regression-tests/properties/todo/valid-deref-stack-1-false.yml b/regression-tests/properties/todo/valid-deref-stack-1-false.yml new file mode 100644 index 0000000..f02037b --- /dev/null +++ b/regression-tests/properties/todo/valid-deref-stack-1-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-deref-stack-1-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-deref + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/todo/valid-deref-stack-1-true.c b/regression-tests/properties/todo/valid-deref-stack-1-true.c new file mode 100644 index 0000000..a51ceec --- /dev/null +++ b/regression-tests/properties/todo/valid-deref-stack-1-true.c @@ -0,0 +1,9 @@ +int* validStackAccess() { + static int a = 10; // Static variable persists beyond the scope of the function + return &a; +} + +void main() { + int *p = validStackAccess(); + *p = 20; // Valid access +} diff --git a/regression-tests/properties/todo/valid-deref-stack-1-true.yml b/regression-tests/properties/todo/valid-deref-stack-1-true.yml new file mode 100644 index 0000000..d6464bf --- /dev/null +++ b/regression-tests/properties/todo/valid-deref-stack-1-true.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-deref-stack-1-true.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: true + subproperty: valid-deref + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/todo/valid-deref-type-1-false.c b/regression-tests/properties/todo/valid-deref-type-1-false.c new file mode 100644 index 0000000..7bf3d9b --- /dev/null +++ b/regression-tests/properties/todo/valid-deref-type-1-false.c @@ -0,0 +1,5 @@ +void main() { + int a = 10; + long *p = (long *)&a; + *p = 20; // Incorrect type access - accessing an 'int' as a 'long' +} diff --git a/regression-tests/properties/todo/valid-deref-type-1-false.yml b/regression-tests/properties/todo/valid-deref-type-1-false.yml new file mode 100644 index 0000000..9dde167 --- /dev/null +++ b/regression-tests/properties/todo/valid-deref-type-1-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-deref-type-1-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-deref + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/todo/valid-deref-type-2-false.c b/regression-tests/properties/todo/valid-deref-type-2-false.c new file mode 100644 index 0000000..40efd8d --- /dev/null +++ b/regression-tests/properties/todo/valid-deref-type-2-false.c @@ -0,0 +1,4 @@ +void main() { + long *p = (long*) malloc(sizeof(int)); + *p = 42; // Incorrect type access - accessing an 'int' as a 'long' +} diff --git a/regression-tests/properties/todo/valid-deref-type-2-false.yml b/regression-tests/properties/todo/valid-deref-type-2-false.yml new file mode 100644 index 0000000..facccc9 --- /dev/null +++ b/regression-tests/properties/todo/valid-deref-type-2-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-deref-type-2-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-deref + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/todo/valid-deref-type-2-true.c b/regression-tests/properties/todo/valid-deref-type-2-true.c new file mode 100644 index 0000000..71b303f --- /dev/null +++ b/regression-tests/properties/todo/valid-deref-type-2-true.c @@ -0,0 +1,3 @@ +void main() { + long *p = (long*) malloc(sizeof(int)); // this is fine, no access. +} diff --git a/regression-tests/properties/todo/valid-deref-type-2-true.yml b/regression-tests/properties/todo/valid-deref-type-2-true.yml new file mode 100644 index 0000000..9291b66 --- /dev/null +++ b/regression-tests/properties/todo/valid-deref-type-2-true.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-deref-type-2-true.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: true + subproperty: valid-deref + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-deref-arraybounds-1-false.c b/regression-tests/properties/valid-deref-arraybounds-1-false.c new file mode 100644 index 0000000..3c43d5d --- /dev/null +++ b/regression-tests/properties/valid-deref-arraybounds-1-false.c @@ -0,0 +1,4 @@ +void main() { + int arr[3] = {1, 2, 3}; + arr[-1] = 42; +} diff --git a/regression-tests/properties/valid-deref-arraybounds-1-false.yml b/regression-tests/properties/valid-deref-arraybounds-1-false.yml new file mode 100644 index 0000000..ec7334e --- /dev/null +++ b/regression-tests/properties/valid-deref-arraybounds-1-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-deref-arraybounds-1-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-deref + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-deref-arraybounds-2-false.c b/regression-tests/properties/valid-deref-arraybounds-2-false.c new file mode 100644 index 0000000..8799469 --- /dev/null +++ b/regression-tests/properties/valid-deref-arraybounds-2-false.c @@ -0,0 +1,4 @@ +void main() { + int arr[3] = {1, 2, 3}; + arr[4] = 42; +} diff --git a/regression-tests/properties/valid-deref-arraybounds-2-false.yml b/regression-tests/properties/valid-deref-arraybounds-2-false.yml new file mode 100644 index 0000000..1bc79e9 --- /dev/null +++ b/regression-tests/properties/valid-deref-arraybounds-2-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-deref-arraybounds-2-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-deref + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-deref-arraybounds-3-false.c b/regression-tests/properties/valid-deref-arraybounds-3-false.c new file mode 100644 index 0000000..1b600e0 --- /dev/null +++ b/regression-tests/properties/valid-deref-arraybounds-3-false.c @@ -0,0 +1,9 @@ +#include +extern int nondet(); + +void main() { + int n = nondet(); + int *arr = (int*) malloc(sizeof(int)*n); + arr[n] = 42; + free(arr); +} diff --git a/regression-tests/properties/valid-deref-arraybounds-3-false.yml b/regression-tests/properties/valid-deref-arraybounds-3-false.yml new file mode 100644 index 0000000..4305375 --- /dev/null +++ b/regression-tests/properties/valid-deref-arraybounds-3-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-deref-arraybounds-3-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-deref + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-deref-arraybounds-3-true.c b/regression-tests/properties/valid-deref-arraybounds-3-true.c new file mode 100644 index 0000000..f43e7b9 --- /dev/null +++ b/regression-tests/properties/valid-deref-arraybounds-3-true.c @@ -0,0 +1,10 @@ +#include +extern int nondet(); + +void main() { + int n = nondet(); + assume(n > 0); + int *arr = (int*) malloc(sizeof(int)*n); + arr[n-1] = 42; + free(arr); +} diff --git a/regression-tests/properties/valid-deref-arraybounds-3-true.yml b/regression-tests/properties/valid-deref-arraybounds-3-true.yml new file mode 100644 index 0000000..020abc1 --- /dev/null +++ b/regression-tests/properties/valid-deref-arraybounds-3-true.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-deref-arraybounds-3-true.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: true + subproperty: valid-deref + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-deref-arraybounds-4-false.c b/regression-tests/properties/valid-deref-arraybounds-4-false.c new file mode 100644 index 0000000..ee3483a --- /dev/null +++ b/regression-tests/properties/valid-deref-arraybounds-4-false.c @@ -0,0 +1,7 @@ +#include + +int arr[10]; + +void main() { + arr[10] = 42; +} diff --git a/regression-tests/properties/valid-deref-arraybounds-4-false.yml b/regression-tests/properties/valid-deref-arraybounds-4-false.yml new file mode 100644 index 0000000..299f36d --- /dev/null +++ b/regression-tests/properties/valid-deref-arraybounds-4-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-deref-arraybounds-4-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-deref + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-deref-nullptr-false.c b/regression-tests/properties/valid-deref-nullptr-false.c new file mode 100644 index 0000000..e42ecb9 --- /dev/null +++ b/regression-tests/properties/valid-deref-nullptr-false.c @@ -0,0 +1,4 @@ +void main() { + int *p = 0; + *p = 42; +} diff --git a/regression-tests/properties/valid-deref-nullptr-false.yml b/regression-tests/properties/valid-deref-nullptr-false.yml new file mode 100644 index 0000000..caeafdf --- /dev/null +++ b/regression-tests/properties/valid-deref-nullptr-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-deref-nullptr-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-deref + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-deref-uninit-false.c b/regression-tests/properties/valid-deref-uninit-false.c new file mode 100644 index 0000000..4e17370 --- /dev/null +++ b/regression-tests/properties/valid-deref-uninit-false.c @@ -0,0 +1,4 @@ +void main() { + int *p; + *p = 42; +} diff --git a/regression-tests/properties/valid-deref-uninit-false.yml b/regression-tests/properties/valid-deref-uninit-false.yml new file mode 100644 index 0000000..d65a335 --- /dev/null +++ b/regression-tests/properties/valid-deref-uninit-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-deref-uninit-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-deref + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/horn-hcc-heap/memtrack-02.c b/regression-tests/properties/valid-free-1-true.c similarity index 73% rename from regression-tests/horn-hcc-heap/memtrack-02.c rename to regression-tests/properties/valid-free-1-true.c index 7babb04..6dc5c0d 100644 --- a/regression-tests/horn-hcc-heap/memtrack-02.c +++ b/regression-tests/properties/valid-free-1-true.c @@ -1,3 +1,5 @@ +#include + void main() { int *x = malloc(sizeof *x); free(x); diff --git a/regression-tests/properties/valid-free-1-true.yml b/regression-tests/properties/valid-free-1-true.yml new file mode 100644 index 0000000..b180b36 --- /dev/null +++ b/regression-tests/properties/valid-free-1-true.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-free-1-true.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: true + subproperty: valid-free + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-free-10-true.c b/regression-tests/properties/valid-free-10-true.c new file mode 100644 index 0000000..fe6c954 --- /dev/null +++ b/regression-tests/properties/valid-free-10-true.c @@ -0,0 +1,9 @@ +#include + +void foo() { + int *x = alloca(sizeof(int)); +} + +void main() { + foo(); +} diff --git a/regression-tests/properties/valid-free-10-true.yml b/regression-tests/properties/valid-free-10-true.yml new file mode 100644 index 0000000..bf28cf5 --- /dev/null +++ b/regression-tests/properties/valid-free-10-true.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-free-10-true.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: true + subproperty: valid-free + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-free-11-true.c b/regression-tests/properties/valid-free-11-true.c new file mode 100644 index 0000000..2d04af2 --- /dev/null +++ b/regression-tests/properties/valid-free-11-true.c @@ -0,0 +1,9 @@ +#include + +void foo() { + int *x = alloca(sizeof(int)*3); +} + +void main() { + foo(); +} diff --git a/regression-tests/properties/valid-free-11-true.yml b/regression-tests/properties/valid-free-11-true.yml new file mode 100644 index 0000000..3c67b46 --- /dev/null +++ b/regression-tests/properties/valid-free-11-true.yml @@ -0,0 +1,13 @@ +format_version: '2.0' + +input_files: 'valid-free-11-true +.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: true + subproperty: valid-free + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-free-2-false.c b/regression-tests/properties/valid-free-2-false.c new file mode 100644 index 0000000..2ee3927 --- /dev/null +++ b/regression-tests/properties/valid-free-2-false.c @@ -0,0 +1,7 @@ +#include + +void main() { + int *x = malloc(sizeof *x); + free(x); + free(x); // double free - undefined behavior +} diff --git a/regression-tests/properties/valid-free-2-false.yml b/regression-tests/properties/valid-free-2-false.yml new file mode 100644 index 0000000..55ffd64 --- /dev/null +++ b/regression-tests/properties/valid-free-2-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-free-2-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-free + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-free-3-true.c b/regression-tests/properties/valid-free-3-true.c new file mode 100644 index 0000000..8d376d1 --- /dev/null +++ b/regression-tests/properties/valid-free-3-true.c @@ -0,0 +1,6 @@ +#include + +void main() { + int *x = 0; + free(x); // OK because x is null pointer. +} diff --git a/regression-tests/properties/valid-free-3-true.yml b/regression-tests/properties/valid-free-3-true.yml new file mode 100644 index 0000000..6e1ed0f --- /dev/null +++ b/regression-tests/properties/valid-free-3-true.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-free-3-true.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: true + subproperty: valid-free + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-free-4-false.c b/regression-tests/properties/valid-free-4-false.c new file mode 100644 index 0000000..d587b3f --- /dev/null +++ b/regression-tests/properties/valid-free-4-false.c @@ -0,0 +1,6 @@ +#include + +void main() { + int *x; + free(x); // not OK, because x is uninitialized and not null. +} diff --git a/regression-tests/properties/valid-free-4-false.yml b/regression-tests/properties/valid-free-4-false.yml new file mode 100644 index 0000000..9435e35 --- /dev/null +++ b/regression-tests/properties/valid-free-4-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-free-4-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-free + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-free-5-false.c b/regression-tests/properties/valid-free-5-false.c new file mode 100644 index 0000000..12c0dc2 --- /dev/null +++ b/regression-tests/properties/valid-free-5-false.c @@ -0,0 +1,7 @@ +#include + +void main() { + int x; + int *y = &x; + free(y); // not OK, because y is a stack pointer. +} diff --git a/regression-tests/properties/valid-free-5-false.yml b/regression-tests/properties/valid-free-5-false.yml new file mode 100644 index 0000000..c4d889b --- /dev/null +++ b/regression-tests/properties/valid-free-5-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-free-5-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-free + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-free-6-true.c b/regression-tests/properties/valid-free-6-true.c new file mode 100644 index 0000000..d89a75b --- /dev/null +++ b/regression-tests/properties/valid-free-6-true.c @@ -0,0 +1,6 @@ +#include + +void main() { + int *x = malloc(sizeof(int)*42); + free(x); +} diff --git a/regression-tests/properties/valid-free-6-true.yml b/regression-tests/properties/valid-free-6-true.yml new file mode 100644 index 0000000..d259940 --- /dev/null +++ b/regression-tests/properties/valid-free-6-true.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-free-6-true.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: true + subproperty: valid-free + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-free-7-false.c b/regression-tests/properties/valid-free-7-false.c new file mode 100644 index 0000000..427c43c --- /dev/null +++ b/regression-tests/properties/valid-free-7-false.c @@ -0,0 +1,6 @@ +#include + +void main() { + int x[42]; + free(x); +} diff --git a/regression-tests/properties/valid-free-7-false.yml b/regression-tests/properties/valid-free-7-false.yml new file mode 100644 index 0000000..d0cccc6 --- /dev/null +++ b/regression-tests/properties/valid-free-7-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-free-7-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-free + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-free-8-false.c b/regression-tests/properties/valid-free-8-false.c new file mode 100644 index 0000000..5154bf4 --- /dev/null +++ b/regression-tests/properties/valid-free-8-false.c @@ -0,0 +1,10 @@ +#include + +void foo() { + int *x = alloca(sizeof(int)); + free(x); +} + +void main() { + foo(); +} diff --git a/regression-tests/properties/valid-free-8-false.yml b/regression-tests/properties/valid-free-8-false.yml new file mode 100644 index 0000000..0c4e243 --- /dev/null +++ b/regression-tests/properties/valid-free-8-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-free-8-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-free + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-free-9-false.c b/regression-tests/properties/valid-free-9-false.c new file mode 100644 index 0000000..9f05ee1 --- /dev/null +++ b/regression-tests/properties/valid-free-9-false.c @@ -0,0 +1,10 @@ +#include + +void foo() { + int *x = alloca(sizeof(int)*3); + free(x); +} + +void main() { + foo(); +} diff --git a/regression-tests/properties/valid-free-9-false.yml b/regression-tests/properties/valid-free-9-false.yml new file mode 100644 index 0000000..9246f30 --- /dev/null +++ b/regression-tests/properties/valid-free-9-false.yml @@ -0,0 +1,12 @@ +format_version: '2.0' + +input_files: 'valid-free-9-false.c' + +properties: + - property_file: ../properties/valid-memsafety.prp + expected_verdict: false + subproperty: valid-free + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-memcleanup-1-false.c b/regression-tests/properties/valid-memcleanup-1-false.c new file mode 100644 index 0000000..2e266b7 --- /dev/null +++ b/regression-tests/properties/valid-memcleanup-1-false.c @@ -0,0 +1,6 @@ +#include + +void main() { + int *p = malloc(sizeof(int)); + // p is not freed before program end - violates memcleanup. +} diff --git a/regression-tests/properties/valid-memcleanup-1-false.yml b/regression-tests/properties/valid-memcleanup-1-false.yml new file mode 100644 index 0000000..8fc7e13 --- /dev/null +++ b/regression-tests/properties/valid-memcleanup-1-false.yml @@ -0,0 +1,11 @@ +format_version: '2.0' + +input_files: 'valid-memcleanup-1-false.c' + +properties: + - property_file: ../properties/valid-memcleanup.prp + expected_verdict: false + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-memcleanup-1-true.c b/regression-tests/properties/valid-memcleanup-1-true.c new file mode 100644 index 0000000..16ffff5 --- /dev/null +++ b/regression-tests/properties/valid-memcleanup-1-true.c @@ -0,0 +1,6 @@ +#include + +void main() { + int *p = malloc(sizeof(int)); + free(p); +} diff --git a/regression-tests/properties/valid-memcleanup-1-true.yml b/regression-tests/properties/valid-memcleanup-1-true.yml new file mode 100644 index 0000000..ad03e4e --- /dev/null +++ b/regression-tests/properties/valid-memcleanup-1-true.yml @@ -0,0 +1,11 @@ +format_version: '2.0' + +input_files: 'valid-memcleanup-1-true.c' + +properties: + - property_file: ../properties/valid-memcleanup.prp + expected_verdict: true + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-memcleanup-array-false.c b/regression-tests/properties/valid-memcleanup-array-false.c new file mode 100644 index 0000000..7891b78 --- /dev/null +++ b/regression-tests/properties/valid-memcleanup-array-false.c @@ -0,0 +1,9 @@ +#include + +void* allocArray(int n) { + return malloc(sizeof(int)*n); +} + +void main() { + int p[] = (int*) allocArray(10); +} diff --git a/regression-tests/properties/valid-memcleanup-array-false.yml b/regression-tests/properties/valid-memcleanup-array-false.yml new file mode 100644 index 0000000..8ee8c5f --- /dev/null +++ b/regression-tests/properties/valid-memcleanup-array-false.yml @@ -0,0 +1,11 @@ +format_version: '2.0' + +input_files: 'valid-memcleanup-array-false.c' + +properties: + - property_file: ../properties/valid-memcleanup.prp + expected_verdict: false + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-memcleanup-array-true.c b/regression-tests/properties/valid-memcleanup-array-true.c new file mode 100644 index 0000000..ed6f99a --- /dev/null +++ b/regression-tests/properties/valid-memcleanup-array-true.c @@ -0,0 +1,18 @@ +#include + +int* allocArray(int n) { + return malloc(sizeof(int)*n); +} + +void freePtr(int *q) { + free(q); +} + +void main() { + int p[] = allocArray(10); + /* Note that int * p = ... does not work, and will be unsafe, + because tricera currently cannot recognize p as an array pointer, + and as a result incorrectly treats AddrRange as Addr sort. + */ + freePtr(p); +} diff --git a/regression-tests/properties/valid-memcleanup-array-true.yml b/regression-tests/properties/valid-memcleanup-array-true.yml new file mode 100644 index 0000000..3a02728 --- /dev/null +++ b/regression-tests/properties/valid-memcleanup-array-true.yml @@ -0,0 +1,11 @@ +format_version: '2.0' + +input_files: 'valid-memcleanup-array-true.c' + +properties: + - property_file: ../properties/valid-memcleanup.prp + expected_verdict: true + +options: + language: C + data_model: ILP32 diff --git a/regression-tests/properties/valid-memtrack-array-true.c b/regression-tests/properties/valid-memtrack-array-true.c new file mode 100644 index 0000000..b20ab02 --- /dev/null +++ b/regression-tests/properties/valid-memtrack-array-true.c @@ -0,0 +1,13 @@ +#include + +void* allocArray(int n) { + return malloc(sizeof(int)*n); +} + +void main() { + int p[] = (int*) allocArray(10); + // This violates memcleanup, but not memtrack. + // Note, if there would have been a return statement, this would + // have violated memtrack too. + // See https://groups.google.com/g/sv-comp/c/Slug4p2DACM/m/ajhC7krvEgAJ +} diff --git a/regression-tests/horn-hcc-array/simple-dynamic-memsafety1.yml b/regression-tests/properties/valid-memtrack-array-true.yml similarity index 81% rename from regression-tests/horn-hcc-array/simple-dynamic-memsafety1.yml rename to regression-tests/properties/valid-memtrack-array-true.yml index 3568bd2..0c2c798 100644 --- a/regression-tests/horn-hcc-array/simple-dynamic-memsafety1.yml +++ b/regression-tests/properties/valid-memtrack-array-true.yml @@ -1,6 +1,6 @@ format_version: '2.0' -input_files: 'simple-dynamic-memsafety1.c' +input_files: 'valid-memtrack-array-true.c' properties: - property_file: ../properties/valid-memsafety.prp diff --git a/regression-tests/quantifiers/Answers b/regression-tests/quantifiers/Answers index a1f3aea..2741c2f 100644 --- a/regression-tests/quantifiers/Answers +++ b/regression-tests/quantifiers/Answers @@ -15,7 +15,6 @@ ext-univ-5-cmpN-safe.hcc SAFE ext-univ-1-unsafe.hcc -UNSAFE -------------------------------------- Init: @@ -40,5 +39,6 @@ Final: main_2(1, store(const(1), 0, 0), 1) -------------------------------------- Failed assertion: -false :- main_2(n:2, a:4, i:5), \exists int v0; (v0 >= 0 & n:2 - v0 >= 1 & select(a:4, v0) != v0 - 1). (line:11 col:3) +false :- main_2(n:2, a:4, i:5), \exists int v0; (v0 >= 0 & n:2 - v0 >= 1 & select(a:4, v0) != v0 - 1). (line:11 col:3) (property: unreach-call) +UNSAFE diff --git a/regression-tests/runalldirs b/regression-tests/runalldirs index 32fc516..0e8b91f 100755 --- a/regression-tests/runalldirs +++ b/regression-tests/runalldirs @@ -24,6 +24,7 @@ run_test ./rundir uninterpreted-predicates "" -assert -dev -t:60 run_test ./rundir math-arrays "" -assert -dev -t:60 run_test ./rundir quantifiers "" -assert -dev -t:60 run_test ./rundir interpreted-predicates "" -assert -dev -t:60 +run_test ./rundir properties "" -assert -dev -t:60 #run_test ./rundir ParametricEncoder "" if [ $ERRORS -ne 0 ]; then diff --git a/regression-tests/uninterpreted-predicates/Answers b/regression-tests/uninterpreted-predicates/Answers index 6f39d88..76af574 100644 --- a/regression-tests/uninterpreted-predicates/Answers +++ b/regression-tests/uninterpreted-predicates/Answers @@ -13,7 +13,6 @@ Warning: no definition of function "nondet" available SAFE unint-pred-simple-false.c -UNSAFE ------------ Init: @@ -28,8 +27,9 @@ Final: main_1(42) ------------ Failed assertion: -false :- main_1(x:5), x:5 != 43. (line:7 col:3) +false :- main_1(x:5), x:5 != 43. (line:7 col:3) (property: user-assertion) +UNSAFE unint-pred-simple-true.c SAFE diff --git a/src/tricera/Main.scala b/src/tricera/Main.scala index 5e86363..85bd6e3 100644 --- a/src/tricera/Main.scala +++ b/src/tricera/Main.scala @@ -1,5 +1,5 @@ /** - * Copyright (c) 2011-2023 Zafer Esen, Hossein Hojjat, Philipp Ruemmer. + * Copyright (c) 2011-2024 Zafer Esen, Hossein Hojjat, Philipp Ruemmer. * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -30,16 +30,20 @@ package tricera +import ap.parser.IExpression.{ConstantTerm, Predicate} +import ap.parser.{IAtom, IConstant, IFormula, VariableSubstVisitor} import hornconcurrency.ParametricEncoder import java.io.{FileOutputStream, PrintStream} +import java.nio.file.{Files, Paths} import lazabs.horn.bottomup.HornClauses.Clause import tricera.concurrency.{CCReader, TriCeraPreprocessor} import lazabs.prover._ import tricera.Util.SourceInfo import tricera.benchmarking.Benchmarking._ -import tricera.concurrency.CCReader.CCClause +import tricera.concurrency.CCReader.{CCAssertionClause, CCClause} import tricera.concurrency.ccreader.CCExceptions._ +import tricera.parsers.YAMLParser._ import sys.process._ @@ -63,13 +67,136 @@ object Main { def doMain(args: Array[String], stoppingCond: => Boolean) : ExecutionSummary = { val triMain = new Main(args) - val res = triMain.run(stoppingCond) - res.executionResult match { - case Safe => // nothing, already printed - case Unsafe => // nothing, already printed - case other => println(other) + + triMain.programTimer.start() + var remainingTimeout : Option[Int] = params.TriCeraParameters.get.timeout + + val (propertiesToCheck, propertyToExpected) = collectProperties + + /** + * @todo Below implementation can be improved a lot - there is no + * need for the reader to parse the input for each property. + */ + val result = if (tricera.params.TriCeraParameters.get.splitProperties && + propertiesToCheck.size > 1) { + println(s"Splitting properties: {${propertiesToCheck.mkString(",")}}") + var remainingProperties = propertiesToCheck + var overallResult = ExecutionSummary(DidNotExecute) + + var prevDuration = triMain.programTimer.s + while(remainingProperties nonEmpty) { + val property = remainingProperties.head + print(s" $property... ") + remainingProperties = remainingProperties.tail + + remainingTimeout = remainingTimeout match { + case Some(to) => Some((to.toDouble - triMain.programTimer.ms).toInt) + case None => None + } + val propertyResult = + triMain.run(stoppingCond, Set(property), propertyToExpected, + remainingTimeout) + val runDuration = propertyResult.elapsedTime - prevDuration + prevDuration = propertyResult.elapsedTime + if (propertyResult.executionResult != DidNotExecute) { + overallResult = ExecutionSummary( + propertyResult.executionResult, + overallResult.propertyResult ++ propertyResult.propertyResult, + overallResult.modelledHeap || propertyResult.modelledHeap, + propertyResult.elapsedTime, // this accumulates between runs + overallResult.preprocessTime + propertyResult.preprocessTime) + if (propertyResult.executionResult != Safe && + propertyResult.executionResult != DidNotExecute) { + // No need to continue if we could not prove this property. + remainingProperties = Set() + } + println(propertyResult.executionResult) + } + } + overallResult + } else { + triMain.run(stoppingCond, propertiesToCheck, propertyToExpected, + remainingTimeout) } - res + println(result.executionResult) + result + } + + private def collectProperties : (Set[properties.Property], + Map[properties.Property, Boolean]) = { + val params = tricera.params.TriCeraParameters.get + import params._ + // Check if an accompanying .yml file exists (SV-COMP style). + val yamlFileName = fileName.replaceAll("\\.[^.]*$", "") + ".yml" + val bmInfo : Option[BenchmarkInfo] = + if (Files.exists(Paths.get(yamlFileName))) { + val info = extractBenchmarkInfo(yamlFileName) + if (info isEmpty) Util.warn( + "Could not parse the accompanying YAML (.yml) file, ignoring it.") + info + } else None + + /** + * Properties to check and their expected status, if any. + */ + val (propertiesToCheck : Set[properties.Property], + propertyToExpected : Map[properties.Property, Boolean]) = { + val cliProps : Set[properties.Property] = Set( + if (checkMemTrack) Some(properties.MemValidTrack) else None, + if (checkValidFree) Some(properties.MemValidFree) else None, + if (checkValidDeref) Some(properties.MemValidDeref) else None, + if (checkMemCleanup) Some(properties.MemValidCleanup) else None, + if (checkReachSafety) Some(properties.Reachability) else None).flatten ++ + (if (checkMemSafety) + memSafetyProperties else Set[properties.Property]()) + + if (cliProps.nonEmpty && bmInfo.nonEmpty) { + Util.warn("A property file exists, but properties are also " + + "specified in the command-line. Ignoring the property file.") + (cliProps, Map.empty[properties.Property, Boolean]) + } else if (bmInfo.nonEmpty) { + // SV-COMP style property specification. + val props = bmInfo.get.properties.flatMap{p => + val verdictOption = p.expected_verdict + p match { + case _ if p.isReachSafety => + verdictOption.map(properties.Reachability -> _) + + case _ if p.isMemSafety => + val initialSubProps = memSafetyProperties.map(_ -> true).toMap + // At most one sub-property is expected to not hold, if any. + val updatedSubProps = verdictOption match { + case Some(false) => p.subproperty match { + case Some("valid-free") => + initialSubProps.updated(properties.MemValidFree, false) + case Some("valid-deref") => + initialSubProps.updated(properties.MemValidDeref, false) + case Some("valid-memtrack") => + initialSubProps.updated(properties.MemValidTrack, false) + case Some(prop) => throw new Exception( + s"Unknown sub-property $prop for the memsafety category.") + case None => throw new Exception( + "The failing sub-property must be specified for memsafety.") + } + case _ => initialSubProps + } + updatedSubProps + case _ if p.isMemCleanup => + verdictOption.map(properties.MemValidCleanup -> _) + + case _ => None + } + }.toMap + + val propsSet : Set[properties.Property] = props.keys.toSet + (propsSet, props) + } else { + // No property file: use CLI properties. If none, use Reachability. + (if (cliProps nonEmpty) cliProps else Set(properties.Reachability), + Map[properties.Property, Boolean]()) + } + } + (propertiesToCheck, propertyToExpected) } private def printError(message: String): Unit = @@ -98,15 +225,18 @@ class Main (args: Array[String]) { private val programTimer = new Timer private val preprocessTimer = new Timer - def run(stoppingCond: => Boolean) : ExecutionSummary = try { + def run(stoppingCond: => Boolean, + propertiesToCheck : Set[properties.Property], + propertyToExpected : Map[properties.Property, Boolean], + runTimeout : Option[Int]) + : ExecutionSummary = try { if (params.doNotExecute) // Exit early if we showed the help return ExecutionSummary(DidNotExecute) - programTimer.start() // work-around: make the Princess wrapper thread-safe lazabs.prover.PrincessWrapper.newWrapper - timeoutChecker = timeout match { + timeoutChecker = runTimeout match { case Some(to) => () => { if (programTimer.ms > to.toDouble) throw TimeoutException @@ -204,72 +334,18 @@ class Main (args: Array[String]) { } preprocessTimer.stop() - // check if an accompanying .yml file exists (SV-COMP style) - case class BMOption(language: String, data_model: String) - case class BMPropertyFile(property_file: String, - expected_verdict: Option[Boolean] = None, - subproperty: Option[String] = None) { - def isReachSafety = property_file.contains("unreach-call") - - def isMemSafety = property_file.contains("valid-memsafety") - } - case class BenchmarkInfo(format_version: String, - input_files: String, - properties: List[BMPropertyFile], - options: BMOption) - val bmInfo: Option[BenchmarkInfo] = try { - import java.nio.file.{Paths, Files} - val yamlFileName = fileName.replaceAll("\\.[^.]*$", "") + ".yml" - if (Files.exists(Paths.get(yamlFileName))) { - // println("Accompanying yaml file found") - import net.jcazevedo.moultingyaml._ - object BenchmarkYamlProtocol extends DefaultYamlProtocol { - implicit val propFormat = yamlFormat3(BMPropertyFile) - implicit val optFormat = yamlFormat2(BMOption) - implicit val bmInfoFormat = yamlFormat4(BenchmarkInfo) - } - import BenchmarkYamlProtocol._ - val src = scala.io.Source.fromFile(yamlFileName) - val yamlAst = src.mkString.stripMargin.parseYaml - src.close - Some(yamlAst.convertTo[BenchmarkInfo]) - } else None - } catch { - case _: Throwable => Util.warn( - "could not parse the accompanying Yaml(.yml) file, ignoring it...") - None - } - - val bmTracks: List[(BenchmarkTrack, Option[Boolean])] = bmInfo match { - case Some(info) => - for (p <- info.properties if p.isMemSafety || p.isReachSafety) yield { - val track = - if (p.isReachSafety) - Reachability - else //(p.isMemSafety) - p.subproperty match { - case Some("valid-free") => MemSafety(Some(ValidFree)) - case Some("valid-deref") => MemSafety(Some(ValidDeref)) - case Some("valid-memtrack") => MemSafety(Some(MemTrack)) - case _ => MemSafety(None) - } - (track, p.expected_verdict) + Console.withOut(outStream){ + println("Checked properties:") + for (prop <- propertiesToCheck) { + print(s" $prop") + propertyToExpected get prop match { + case Some(expected) => println(s" (expected: $expected)") + case None => println } - case None => Nil - } - - if (bmInfo.nonEmpty && bmTracks.isEmpty) { - return ExecutionSummary(DidNotExecute, preprocessTime = preprocessTimer.s) - //throw new MainException("An associated property file (.yml) is " + - // "found, however TriCera currently can only check for unreach-call" + - // " and a subset of valid-memsafety properties.") + } + println } - if (bmTracks.exists(t => t._1 match { - case MemSafety(Some(MemTrack)) => true - case MemSafety(Some(ValidFree)) => true - case _ => false - })) shouldTrackMemory = true // todo: pass string to TriCera instead of writing to and passing file? // todo: add a switch for this, also benchmark/profile @@ -277,13 +353,15 @@ class Main (args: Array[String]) { new java.io.FileReader(new java.io.File(ppFileName)))) val (reader, modelledHeapRes) = try { - CCReader(bufferedReader, funcName, shouldTrackMemory) + CCReader(bufferedReader, funcName, propertiesToCheck) } catch { - case e: ParseException if !devMode => - return ExecutionSummary(ParseError(e.getMessage), Nil, modelledHeap, 0, preprocessTimer.s) - case e: TranslationException if !devMode => - return ExecutionSummary(TranslationError(e.getMessage), Nil, modelledHeap, 0, preprocessTimer.s) - case e: Throwable => throw e + case e : ParseException if !devMode => + return ExecutionSummary(ParseError(e.getMessage), Map(), + modelledHeap, 0, preprocessTimer.s) + case e : TranslationException if !devMode => + return ExecutionSummary(TranslationError(e.getMessage), Map(), + modelledHeap, 0, preprocessTimer.s) + case e : Throwable => throw e } if (printPathConstraints) { @@ -375,15 +453,26 @@ class Main (args: Array[String]) { tricera.concurrency.ReaderMain.printSMTClauses(smallSystem) if(prettyPrint || smtPrettyPrint || printPathConstraints) - return ExecutionSummary(DidNotExecute, Nil, modelledHeap, 0, preprocessTimer.s) + return ExecutionSummary(DidNotExecute, Map(), modelledHeap, 0, preprocessTimer.s) + /** + * Expected status is printed in SMT files when they are dumped. + */ val expectedStatus = - // sat if no tracks are false, unsat otherwise - if (bmTracks.nonEmpty) { - if (bmTracks.forall { track => !track._2.contains(false) }) "sat" + // sat if no properties are expected to be false, unsat otherwise + if (propertiesToCheck.forall(propertyToExpected.contains)) { + if (propertyToExpected.filter( + pair => propertiesToCheck.contains(pair._1)).forall(_._2)) "sat" else "unsat" } else "unknown" + val smtFileName = if (splitProperties) { + assert(propertiesToCheck.size == 1) + s"$fileName-${propertiesToCheck.head}.smt2" + } else { + s"$fileName.smt2" + } + val verificationLoop = try { Console.withOut(outStream) { @@ -391,7 +480,7 @@ class Main (args: Array[String]) { system = smallSystem, initialInvariants = null, printIntermediateClauseSets = printIntermediateClauseSets, - fileName = fileName + ".smt2", + fileName = smtFileName, expectedStatus = expectedStatus, log = needFullSolution, templateBasedInterpolation = templateBasedInterpolation, @@ -415,11 +504,10 @@ class Main (args: Array[String]) { val result = verificationLoop.result if (printIntermediateClauseSets) - return ExecutionSummary(DidNotExecute, Nil, modelledHeap, 0, preprocessTimer.s) + return ExecutionSummary(DidNotExecute, Map(), modelledHeap, 0, preprocessTimer.s) val executionResult = result match { case Left(res) => - println("SAFE") res match { case Some(solution) => import tricera.postprocessor._ @@ -427,34 +515,30 @@ class Main (args: Array[String]) { import lazabs.horn.bottomup.HornPredAbs import lazabs.ast.ASTree.Parameter - def replaceArgs(f : String, - acslArgNames : Seq[String], - replaceAlphabetic : Boolean = false) = { - var s = f - for ((acslArg, ind)<- acslArgNames zipWithIndex) { - val replaceArg = - if (replaceAlphabetic) - lazabs.viewer.HornPrinter.getAlphabeticChar(ind) - else "_" + ind - s = s.replace(replaceArg, acslArg) + def clausifySolution(predAndSol : (Predicate, IFormula), + argNames : Seq[String], + newPredName : Option[String] = None) : Clause = { + val (pred, sol) = predAndSol + val predArgs = for (predArgName <- argNames) yield + IConstant(new ConstantTerm(predArgName)) + val constraint = VariableSubstVisitor.visit( + sol, (predArgs.toList, 0)).asInstanceOf[IFormula] + val newPred = newPredName match { + case Some(newName) => new Predicate(newName, pred.arity) + case None => pred } - s + Clause(IAtom(newPred, predArgs), Nil, constraint) } if(displaySolutionProlog) { - // todo: replace args with actual ones from the clauses println("\nSolution (Prolog)") println("="*80) val sortedSol = solution.toArray.sortWith(_._1.name < _._1.name) for((pred,sol) <- sortedSol) { - val cl = HornClause(RelVar(pred.name.stripPrefix("inv_"), - (0 until pred.arity).map(p => - Parameter("_" + p,lazabs.types.IntegerType())).toList), - List(Interp(lazabs.prover.PrincessWrapper.formula2Eldarica(sol, - Map[ap.terfor.ConstantTerm,String]().empty,false)))) - println(replaceArgs(lazabs.viewer.HornPrinter.print(cl), - reader.PredPrintContext.predArgNames(pred), - replaceAlphabetic = true)) + val predArgNames = reader.PredPrintContext.predArgNames(pred) + val solClause = clausifySolution( + (pred, sol), predArgNames, Some(pred.name.stripPrefix("inv_"))) + println(solClause.toPrologString) } println("="*80 + "\n") } @@ -504,15 +588,18 @@ class Main (args: Array[String]) { if maybeEnc.isEmpty || !maybeEnc.get.prePredsToReplace.contains(ctx.prePred.pred) && !maybeEnc.get.postPredsToReplace.contains(ctx.postPred.pred)) { - val fPre = ACSLLineariser asString processedSolution(ctx.prePred.pred) - val fPost = ACSLLineariser asString processedSolution(ctx.postPred.pred) - // todo: implement replaceArgs as a solution processor - // replaceArgs does a simple string replacement (see above def) - val fPreWithArgs = - replaceArgs(fPre, ctx.prePredACSLArgNames) - val fPostWithArgs = - replaceArgs(fPost, ctx.postPredACSLArgNames) + def funContractToACSLString(fPred : Predicate, + argNames : Seq[String]) : String = { + val fPredToSol = fPred -> processedSolution(fPred) + val fPredClause = clausifySolution(fPredToSol, argNames) + ACSLLineariser asString fPredClause.constraint + } + val fPreACSLString = funContractToACSLString( + ctx.prePred.pred, ctx.prePredACSLArgNames) + + val fPostACSLString = funContractToACSLString( + ctx.postPred.pred, ctx.postPredACSLArgNames) if (!printedACSLHeader) { println("\nInferred ACSL annotations") @@ -521,17 +608,17 @@ class Main (args: Array[String]) { } println("/* contracts for " + fun + " */") println("/*@") - print( " requires "); println(fPreWithArgs + ";") - print( " ensures "); println(fPostWithArgs + ";") + print( " requires "); println(fPreACSLString + ";") + print( " ensures "); println(fPostACSLString + ";") println("*/") } if(loopInvariants nonEmpty) { println("/* loop invariants */") for ((name, (inv, srcInfo)) <- loopInvariants) { - val fInv = ACSLLineariser asString processedSolution.find(p => - p._1.name.stripPrefix("inv_") == inv.pred.name).get._2 - val fInvWithArgs = - replaceArgs(fInv, inv.argVars.map(_.name)) + val fInvSol = processedSolution.find( + p => p._1.name.stripPrefix("inv_") == inv.pred.name).get + val fInvString = ACSLLineariser asString clausifySolution( + fInvSol, inv.argVars.map(_.name), Some(name)).constraint if (!printedACSLHeader) { println("\nInferred ACSL annotations") println("=" * 80) @@ -540,7 +627,7 @@ class Main (args: Array[String]) { println("\n/* loop invariant for the loop at line " + srcInfo.line + " */") println("/*@") - print( " loop invariant "); println(fInvWithArgs + ";") + print( " loop invariant "); println(fInvString + ";") println("*/") } } @@ -552,15 +639,11 @@ class Main (args: Array[String]) { } Safe case Right(cex) => { - println("UNSAFE") - - import hornconcurrency.VerificationLoop._ - import tricera.Util.SourceInfo - import lazabs.horn.bottomup.HornClauses - - val clauseToUnmergedRichClauses : Map[Clause, Seq[CCClause]] = cex._2.iterator.map { + val clauseToUnmergedRichClauses : Map[Clause, Seq[CCClause]] = + cex._2.iterator.map{ case (_, clause) => - val richClauses : Seq[CCClause]= mergedToOriginal get clause match { + val richClauses : Seq[CCClause] = mergedToOriginal get clause + match { case Some(clauses) => for (Some(richClause) <- clauses map reader.getRichClause) yield richClause @@ -573,8 +656,18 @@ class Main (args: Array[String]) { (clause -> richClauses) }.toMap + val violatedAssertionClause = cex._2.head._2 + val violatedRichAssertionClause = + clauseToUnmergedRichClauses get violatedAssertionClause match { + case Some(richClauses) if richClauses != Nil => + assert(richClauses.size == 1) + Some(richClauses.head.asInstanceOf[CCAssertionClause]) + case _ => None + } + if (plainCEX) { - if (cex._1 == Nil) { // todo: print cex when hornConcurrency no longer returns Nil + if (cex._1 == Nil) { // todo: print cex when hornConcurrency no + // longer returns Nil println("This counterexample cannot be printed in the " + "console, use -eogCEX for a graphical view.") } @@ -582,21 +675,20 @@ class Main (args: Array[String]) { println hornconcurrency.VerificationLoop.prettyPrint(cex) if (system.processes.size == 1 && - system.processes.head._2 == ParametricEncoder.Singleton) { // todo: print failed assertion for concurrent systems - val violatedAssertionClause = cex._2.head._2 - clauseToUnmergedRichClauses get violatedAssertionClause match { - case Some(richClauses) if richClauses != Nil => - assert(richClauses.size == 1) - println("Failed assertion:\n" + richClauses.head.toString) + system.processes.head._2 == ParametricEncoder.Singleton) { // + // todo: print failed assertion for concurrent systems + violatedRichAssertionClause match { + case Some(assertionClause) => + println("Failed assertion:\n" + assertionClause.toString) println - case None => + case None => } } } } if (!pngNo) { // dotCEX and maybe eogCEX - if(system.processes.size == 1 && - system.processes.head._2 == ParametricEncoder.Singleton) { + if (system.processes.size == 1 && + system.processes.head._2 == ParametricEncoder.Singleton) { Util.show(cex._2, "cex", clauseToUnmergedRichClauses.map(c => (c._1 -> c._2.filter(_.srcInfo.nonEmpty).map(_.srcInfo.get))), @@ -604,29 +696,38 @@ class Main (args: Array[String]) { reader.PredPrintContext.predSrcInfo, reader.PredPrintContext.isUninterpretedPredicate) } else { - println("Cannot display -eogCEX for concurrent processes, try -cex.") + println("Cannot display -eogCEX for concurrent processes, try " + + "-cex.") } } - Unsafe + if (propertiesToCheck.contains(properties.MemValidTrack) + && params.useMemCleanupForMemTrack) { + if (system.processes.length > 1) { + println("Checking memtrack property with more than one process is" + + " not supported.") + Unknown("concurrency - cannot check memtrack") + } else if (violatedRichAssertionClause.nonEmpty && + violatedRichAssertionClause.get.property == + properties.MemValidCleanup) { + /** + * The stronger property valid-memcleanup was violated, we cannot + * conclude that the weaker valid-memtrack is also violated. + */ + Unknown("memcleanup violated - memtrack inconclusive") + } else Unsafe + } else Unsafe } } - def getExpectedVerdict (expected : Option[Boolean]) : Boolean = - expected match { - case Some(verdict) => verdict - case None => throw new MainException("Benchmark information provided" + - "with no expected verdict!") - } def printVerdictComparison(comparison : Boolean) : Unit = - if (comparison) println(" expected verdict matches the result!") - else println(" expected verdict mismatch!") - - val trackResult = for (track <- bmTracks) yield { - println(track._1) - val expectedVerdict = getExpectedVerdict(track._2) - val verdictMatches = expectedVerdict == result.isLeft - printVerdictComparison(verdictMatches) - (track._1, expectedVerdict) + if (comparison) println(" expected verdict matches the result.") + else println(" expected verdict mismatch.") + + val trackResult = for ((prop, expected) <- propertyToExpected) yield { +// println(prop) + val verdictMatches = expected == result.isLeft +// printVerdictComparison(verdictMatches) + (prop, verdictMatches) } ExecutionSummary(executionResult, trackResult, modelledHeap, @@ -642,30 +743,30 @@ class Main (args: Array[String]) { } catch { case TimeoutException | StoppedException => - ExecutionSummary(Timeout, Nil, modelledHeap, + ExecutionSummary(Timeout, Map(), modelledHeap, programTimer.s, preprocessTimer.s) // nothing case _: java.lang.OutOfMemoryError => printError(OutOfMemory.toString) - ExecutionSummary(OutOfMemory, Nil, modelledHeap, + ExecutionSummary(OutOfMemory, Map(), modelledHeap, programTimer.s, preprocessTimer.s) case t: java.lang.StackOverflowError => if(devMode) t.printStackTrace printError(StackOverflow.toString) - ExecutionSummary(StackOverflow, Nil, modelledHeap, + ExecutionSummary(StackOverflow, Map(), modelledHeap, programTimer.s, preprocessTimer.s) case t: Exception => if(devMode) t.printStackTrace printError(t.getMessage) - ExecutionSummary(OtherError(t.getMessage), Nil, modelledHeap, + ExecutionSummary(OtherError(t.getMessage), Map(), modelledHeap, programTimer.s, preprocessTimer.s) case t: AssertionError => printError(t.getMessage) if(devMode) t.printStackTrace - ExecutionSummary(OtherError(t.getMessage), Nil, modelledHeap, + ExecutionSummary(OtherError(t.getMessage), Map(), modelledHeap, programTimer.s, preprocessTimer.s ) } diff --git a/src/tricera/Util.scala b/src/tricera/Util.scala index 7698b93..752ea9e 100644 --- a/src/tricera/Util.scala +++ b/src/tricera/Util.scala @@ -1,5 +1,5 @@ /** - * Copyright (c) 2021-2023 Zafer Esen, Philipp Ruemmer. All rights reserved. + * Copyright (c) 2021-2024 Zafer Esen, Philipp Ruemmer. All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are met: @@ -122,7 +122,7 @@ object Util { def getLineString(maybeSourceInfo : Option[SourceInfo]) : String = { maybeSourceInfo match { case Some(sourceInfo) => - s"At ${sourceInfo.line}:${sourceInfo.col}: " + s"At (${sourceInfo.line}:${sourceInfo.col}): " case None => "" } } diff --git a/src/tricera/acsl/Encoder.scala b/src/tricera/acsl/Encoder.scala index 3671aac..e70ef17 100644 --- a/src/tricera/acsl/Encoder.scala +++ b/src/tricera/acsl/Encoder.scala @@ -1,5 +1,6 @@ /** - * Copyright (c) 2021-2022 Pontus Ernstedt. All rights reserved. + * Copyright (c) 2021-2022 Pontus Ernstedt + * 2024 Zafer Esen. All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are met: @@ -40,7 +41,7 @@ import tricera.Util.SourceInfo import scala.collection.{Map, Set} import tricera.concurrency.CCReader -import tricera.concurrency.CCReader.CCClause +import tricera.concurrency.CCReader.{CCAssertionClause, CCClause} // FIXME: Maybe just object? Or create companion? @@ -77,7 +78,8 @@ class Encoder(reader : CCReader) { val processes : ProcessSet = if (hasACSLEntryFunction) encodeProcessesEntry else encodeProcesses - asserts.foreach(cc => reader.addRichClause(cc.clause, cc.srcInfo)) + asserts.foreach(cc => reader.mkRichAssertionClause( + cc.clause, cc.srcInfo, cc.property)) system.copy( assertions = asserts.map(_.clause), @@ -95,16 +97,19 @@ class Encoder(reader : CCReader) { * @return encoded assertions and a backmapping from these to the original * clauses */ - private def encodeAssertions : Seq[CCClause] = { - val (preClauses, others) : (Seq[Clause], Seq[Clause]) = + private def encodeAssertions : Seq[CCAssertionClause] = { + val (preClauses, others) : (Seq[Clause], Seq[Clause]) = { system.assertions.partition(c => { prePredsToReplace(c.head.pred) }) + } - val newPreClauses : Seq[CCClause] = + val newPreClauses : Seq[CCAssertionClause] = preClauses.map(c => buildPreClause(reader.getRichClause(c).get)) - val newPostClauses : Seq[CCClause] = buildPostAsserts - (others.map(c => reader.getRichClause(c).get) ++ newPreClauses ++ newPostClauses) + val newPostClauses : Seq[CCAssertionClause] = buildPostAsserts + others.map( + c => reader.getRichClause(c).get.asInstanceOf[CCAssertionClause]) ++ + newPreClauses ++ newPostClauses } /** @@ -126,8 +131,8 @@ class Encoder(reader : CCReader) { val preAtom : IAtom = funToPreAtom(name) val preCond : IFormula = funToContract(name).pre val constr : IFormula = applyArgs(preCond, preAtom, atom) - CCClause(Clause(head, List(), constr), - reader.getRichClause(c).get.srcInfo) + new CCClause(Clause(head, List(), constr), + reader.getRichClause(c).get.srcInfo) } case c@Clause(head, body, oldConstr) if prePredsToReplace(head.pred) => { @@ -198,28 +203,30 @@ class Encoder(reader : CCReader) { ) case _ => (constr, oldSrcInfo) } - CCClause(Clause(head, keep, maybeNewConstr), newSrcInfo) + new CCClause(Clause(head, keep, maybeNewConstr), newSrcInfo) } // Handles function calls, e.g: // f_pre(..) :- mainN(..), .. ==> false :- mainN(..), .., !
-  private def buildPreClause(old : CCClause) : CCClause = {
+  private def buildPreClause(old : CCClause) : CCAssertionClause = {
     assert(prePredsToReplace(old.clause.head.pred))
     val name    : String   = old.clause.head.pred.name.stripSuffix(preSuffix)
     val preCond : IFormula = funToContract(name).pre
     val preAtom : IAtom    = funToPreAtom(name)
     val constr  : IFormula = applyArgs(preCond, preAtom, old.clause.head).unary_!
-    CCClause(Clause(falseHead, old.clause.body, constr), old.srcInfo)
+    reader.mkRichAssertionClause(Clause(falseHead, old.clause.body, constr),
+                              old.srcInfo,
+                              tricera.properties.FunctionPrecondition(name, old.srcInfo))
   }
 
   // Fetches clauses from system.processes and system.backgroundAxioms implying
   // post-condition and generates assertion clauses (to be moved into
   // system.assertions).
-  private def buildPostAsserts : Seq[CCClause] = {
+  private def buildPostAsserts : Seq[CCAssertionClause] = {
     import ParametricEncoder.{NoBackgroundAxioms, SomeBackgroundAxioms}
     val clauses1 : Seq[CCClause] =
       system.processes.flatMap({
-        case (p, r) => p.unzip._1.map(c => reader.getRichClause(c).get)
+        case (p, r) => p.map(p => reader.getRichClause(p._1).get)
       })
     val clauses2 : Seq[CCClause] =
       system.backgroundAxioms match {
@@ -232,7 +239,8 @@ class Encoder(reader : CCReader) {
     clauses.collect({
       // Handles final clause, e.g:
       // f_post(..) :- f1(..) ==> false :- f1(..), !( & )
-      case CCClause(Clause(head, body, oldConstr), _) if postPredsToReplace(head.pred) => {
+      case CCClause(Clause(head, body, oldConstr), srcInfo)
+        if postPredsToReplace(head.pred) =>
         val name     : String   = head.pred.name.stripSuffix(postSuffix)
         val postAtom : IAtom    = funToPostAtom(name)
         val postCond : IFormula = funToContract(name).post
@@ -240,12 +248,13 @@ class Encoder(reader : CCReader) {
         val constr   : IFormula = applyArgs(postCond, postAtom, head)
         val assigns  : IFormula =
           applyArgs(funToContract(name).assignsAssert, postAtom, head)
-        CCClause(Clause(falseHead, body, oldConstr &&& (constr &&& assigns).unary_!), Some(postSrc))
-      }
+        reader.mkRichAssertionClause(Clause(
+          falseHead, body, oldConstr &&& (constr &&& assigns).unary_!),
+                                  Some(postSrc),
+                                  tricera.properties.FunctionPostcondition(name, srcInfo))
     })
   }
 
-
   private def applyArgs(formula : IFormula, predParams : IAtom, predArgs : IAtom) : IFormula = {
     val paramToArgMap : Map[ITerm, ITerm] =
       predParams.args.zip(predArgs.args).toMap
diff --git a/src/tricera/benchmarking/Benchmarking.scala b/src/tricera/benchmarking/Benchmarking.scala
index 358ecf6..a0fc373 100644
--- a/src/tricera/benchmarking/Benchmarking.scala
+++ b/src/tricera/benchmarking/Benchmarking.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2021-2022 Zafer Esen. All rights reserved.
+ * Copyright (c) 2021-2024 Zafer Esen. All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -29,6 +29,8 @@
 
 package tricera.benchmarking
 
+import tricera.properties
+
 object Benchmarking {
   // Execution Results
   sealed trait ExecutionError
@@ -67,9 +69,9 @@ object Benchmarking {
     override def toString : String =
       "UNSAFE"
   }
-  case object Unknown extends ExecutionResult {
+  case class Unknown(reason : String = "") extends ExecutionResult {
     override def toString: String =
-      "UNKNOWN"
+      "UNKNOWN" + (if(reason.nonEmpty) s" ($reason)" else "")
   }
   case object DidNotExecute extends ExecutionResult {
     override def toString : String =
@@ -77,41 +79,15 @@ object Benchmarking {
     ""
   }
 
-  // SV-COMP related, should probably move somewhere else...
-  // supported SV-COMP benchmark tracks
-  sealed trait BenchmarkTrack
-  case object Reachability extends BenchmarkTrack { // unreachability of error
-    override def toString : String = "unreach-call"
-  }
-  // no subtracks need to be provided on a pass, a single subtrack is provided
-  // on fail
-  case class MemSafety(subTrack : Option[MemSubTrack]) extends BenchmarkTrack {
-    override def toString : String =
-      "valid-memsafety" + (subTrack match {
-        case Some(t) => "/" + t.toString
-        case None => ""
-      })
-  }
-  sealed trait MemSubTrack
-  case object MemTrack extends MemSubTrack { // valid-memtrack
-    override def toString : String = "valid-memtrack"
-  }
-  case object ValidDeref extends MemSubTrack { // valid-deref
-    override def toString : String = "valid-deref"
-  }
-  case object ValidFree extends MemSubTrack { // valid-free
-    override def toString : String = "valid-free"
-  }
-
   // returned by Main
   case class ExecutionSummary (
-                                executionResult: ExecutionResult,
-                                // if a supported SV-COMP track is provided, returns a list of these tracks
-                                // and whether the execution result matched the expected verdict or not
-                                trackResult : List[(BenchmarkTrack, Boolean)] = Nil,
-                                modelledHeap : Boolean = false, // true if the bm contained heap operations
-                                elapsedTime  : Double = 0,
-                                preprocessTime : Double = 0
+    executionResult : ExecutionResult,
+    // if a supported SV-COMP track is provided, returns a list of these tracks
+    // and whether the execution result matched the expected verdict or not
+    propertyResult  : Map[properties.Property, Boolean] = Map(),
+    modelledHeap    : Boolean = false, // true if the bm contained heap operations
+    elapsedTime     : Double = 0,
+    preprocessTime  : Double = 0
                               ) {
     override def toString: String = {
       "Result   : " + executionResult + "\n" +
diff --git a/src/tricera/concurrency/CCReader.scala b/src/tricera/concurrency/CCReader.scala
index 62bb3ab..4d21719 100644
--- a/src/tricera/concurrency/CCReader.scala
+++ b/src/tricera/concurrency/CCReader.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2015-2023 Zafer Esen, Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2015-2024 Zafer Esen, Philipp Ruemmer. All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -50,6 +50,7 @@ import tricera.params.TriCeraParameters
 import tricera.parsers.AnnotationParser
 import tricera.parsers.AnnotationParser._
 import CCExceptions._
+import tricera.{Util, properties}
 
 object CCReader {
   private[concurrency] var useTime = false
@@ -60,7 +61,9 @@ object CCReader {
   private[concurrency] val GTU = new CCVar("_GTU", None, CCInt)
 
   def apply(input : java.io.Reader, entryFunction : String,
-            trackMemorySafety : Boolean = false) : (CCReader, Boolean) = { // second ret. arg is true if modelled heap
+            propertiesToCheck : Set[properties.Property] = Set(
+              properties.Reachability))
+  : (CCReader, Boolean) = { // second ret. arg is true if modelled heap
     def entry(parser : concurrent_c.parser) = parser.pProgram
     val prog = parseWithEntry(input, entry _)
 //    println(printer print prog)
@@ -68,14 +71,13 @@ object CCReader {
     var reader : CCReader = null
     while (reader == null)
       try {
-        reader = new CCReader(prog, entryFunction, trackMemorySafety)
+        reader = new CCReader(prog, entryFunction, propertiesToCheck)
       } catch {
         case NeedsTimeException => {
           warn("enabling time")
           useTime = true
         }
         case NeedsHeapModelException => {
-          warn("enabling heap model")
           modelHeap = true
         }
       }
@@ -92,6 +94,9 @@ object CCReader {
 
     try { entry(p) } catch {
       case e : Exception =>
+        Util.warn(
+"""The input program could not be parsed. If 'main' is not the entry point to
+   |the program, use the option '-m:entry-function-name' to specify the entry point.""".stripMargin)
         throw new ParseException(
              "At line " + String.valueOf(l.line_num()) +
              ", near \"" + l.buff() + "\" :" +
@@ -109,9 +114,8 @@ object CCReader {
     val Mathematical, ILP32, LP64, LLP64 = Value
   }
   //////////////////////////////////////////////////////////////////////////////
-
-  case class CCClause (clause : HornClauses.Clause,
-                       srcInfo : Option[SourceInfo]) { // todo: what else would be useful?
+  class CCClause(val clause  : HornClauses.Clause,
+                 val srcInfo : Option[SourceInfo]) {
     override def toString : String =
       clause.toPrologString + (srcInfo match {
         case None => ""
@@ -119,6 +123,19 @@ object CCReader {
           s" (line:$line col:$col)"
       })
   }
+  object CCClause {
+    def unapply(clause : CCClause)
+    : Option[(HornClauses.Clause, Option[SourceInfo])] =
+      Some((clause.clause, clause.srcInfo))
+  }
+
+  class CCAssertionClause(clause   : HornClauses.Clause,
+                          srcInfo  : Option[SourceInfo],
+                          val property : properties.Property)
+  extends CCClause(clause, srcInfo) {
+    override def toString : String =
+      super.toString + s" (property: $property)"
+  }
 
   // a wrapper for IExpression.Predicate that keeps more info about arguments
   case class CCPredicate(pred : Predicate, argVars : Seq[CCVar],
@@ -147,9 +164,9 @@ object CCReader {
 
 ////////////////////////////////////////////////////////////////////////////////
 
-class CCReader private (prog : Program,
-                        entryFunction : String,
-                        trackMemorySafety : Boolean) {
+class CCReader private (prog              : Program,
+                        entryFunction     : String,
+                        propertiesToCheck : Set[properties.Property]) {
 
   import CCReader._
 
@@ -178,6 +195,7 @@ class CCReader private (prog : Program,
     }
     def size : Int = vars.size
     def lastIndexWhere(name : String) = vars lastIndexWhere(_.name == name)
+    def lastIndexWhere(v : CCVar) = vars lastIndexWhere(_ == v)
     def contains (c : ConstantTerm) = vars exists (_.term == c)
     def iterator = vars.iterator
     def formalVars = vars.toList
@@ -185,10 +203,10 @@ class CCReader private (prog : Program,
     def formalTypes = vars.map(_.typ).toList
   }
 
-  private object globalVars extends CCVars {
+  private object GlobalVars extends CCVars {
     val inits = new ArrayBuffer[CCExpr]
   }
-  private object localVars extends CCVars {
+  private object LocalVars extends CCVars {
     val frameStack = new Stack[Int]
 
     override def addVar (v : CCVar) : Int = {
@@ -199,16 +217,16 @@ class CCReader private (prog : Program,
       vars.update(idx, elem)
     }
     def pop(n : Int) = {
-      localVars trimEnd n
+      LocalVars trimEnd n
       variableHints trimEnd n
-      assert(variableHints.size == size + globalVars.size)
+      assert(variableHints.size == size + GlobalVars.size)
     }
 
     def lastOption : Option[CCVar] = vars.lastOption
     def last : CCVar = vars.last
     def remove(n : Int): CCVar = {
       assume(n >= 0 && n < size)
-      variableHints.remove(n + globalVars.size)
+      variableHints.remove(n + GlobalVars.size)
       vars.remove(n)
     }
     def trimEnd(n: Int) = vars trimEnd n
@@ -216,7 +234,7 @@ class CCReader private (prog : Program,
     def popFrame = {
       val newSize = frameStack.pop
       vars reduceToSize newSize
-      variableHints reduceToSize (globalVars.size + newSize)
+      variableHints reduceToSize (GlobalVars.size + newSize)
     }
     def getVarsInTopFrame : List[CCVar] =
       (vars takeRight (vars.size - frameStack.last)).toList
@@ -224,13 +242,13 @@ class CCReader private (prog : Program,
 
   private def updateVarType(name : String, newType : CCType) = {
     val ind = lookupVar(name)
-    if (ind < globalVars.size) {
-      val oldVar = globalVars.vars(ind)
-      globalVars.vars(ind) =
+    if (ind < GlobalVars.size) {
+      val oldVar = GlobalVars.vars(ind)
+      GlobalVars.vars(ind) =
         new CCVar(name, oldVar.srcInfo, newType)
     } else {
-      val oldVar = localVars.vars(ind - globalVars.size)
-      localVars.vars(ind - globalVars.size) =
+      val oldVar = LocalVars.vars(ind - GlobalVars.size)
+      LocalVars.vars(ind - GlobalVars.size) =
         new CCVar(name, oldVar.srcInfo, newType)
     }
   }
@@ -239,9 +257,9 @@ class CCReader private (prog : Program,
   private val globalExitPred = newPred("exit", Nil, None)
 
   private def lookupVarNoException(name : String) : Int =
-    localVars lastIndexWhere name match {
-      case -1 => globalVars lastIndexWhere name
-      case i  => i + globalVars.size
+    LocalVars lastIndexWhere name match {
+      case -1 => GlobalVars lastIndexWhere name
+      case i  => i + GlobalVars.size
     }
 
   private def lookupVar(name : String) : Int = {
@@ -264,24 +282,24 @@ class CCReader private (prog : Program,
   }
 
   private def allFormalVars : Seq[CCVar] =
-    globalVars.formalVars ++ localVars.formalVars
+    GlobalVars.formalVars ++ LocalVars.formalVars
   private def allFormalVarTerms : Seq[ITerm] =
-    globalVars.formalVarTerms ++ localVars.formalVarTerms
+    GlobalVars.formalVarTerms ++ LocalVars.formalVarTerms
   private def allFormalVarTypes : Seq[CCType] =
-    globalVars.formalTypes ++ localVars.formalTypes
+    GlobalVars.formalTypes ++ LocalVars.formalTypes
 
   private def allFormalExprs : Seq[CCExpr] =
-    ((for (v <- globalVars.iterator)
+    ((for (v <- GlobalVars.iterator)
       yield CCTerm(v.term, v.typ, v.srcInfo)) ++
-     (for (v <- localVars.iterator)
+     (for (v <- LocalVars.iterator)
       yield CCTerm(v.term, v.typ, v.srcInfo))).toList
   private def allVarInits : Seq[ITerm] =
-    (globalVars.inits.toList map (_.toTerm)) ++
-      (localVars.formalVarTerms map (IExpression.i(_)))
+    (GlobalVars.inits.toList map (_.toTerm)) ++
+      (LocalVars.formalVarTerms map (IExpression.i(_)))
 
   private def freeFromGlobal(t : IExpression) : Boolean =
     !ContainsSymbol(t, (s:IExpression) => s match {
-                      case IConstant(c) => globalVars contains c // todo: true only with concurrency?
+                      case IConstant(c) => GlobalVars contains c // todo: true only with concurrency?
                       case _ => false
                     })
 
@@ -337,7 +355,7 @@ class CCReader private (prog : Program,
   private val functionPostOldArgs = new MHashMap[String, Seq[CCVar]]
   private val functionClauses =
     new MHashMap[String, Seq[(Clause, ParametricEncoder.Synchronisation)]]
-  private val functionAssertionClauses = new MHashMap[String, Seq[CCClause]]
+  private val functionAssertionClauses = new MHashMap[String, Seq[CCAssertionClause]]
   private val uniqueStructs = new MHashMap[Unique, String]
   private val structInfos   = new ArrayBuffer[StructInfo]
   private val structDefs    = new MHashMap[String, CCStruct]
@@ -364,10 +382,21 @@ class CCReader private (prog : Program,
 
   //////////////////////////////////////////////////////////////////////////////
 
-  private[tricera] def addRichClause (clause : Clause,
-                     srcInfo : Option[SourceInfo]) : CCClause = {
-    val richClause = CCClause(clause, srcInfo)
-    clauseToRichClause += ((clause, richClause))
+  private[tricera]
+  def addRichClause(clause  : Clause,
+                    srcInfo : Option[SourceInfo]) : CCClause = {
+    val richClause = new CCClause(clause, srcInfo)
+    clauseToRichClause += clause -> richClause
+    richClause
+  }
+
+  private[tricera]
+  def mkRichAssertionClause(clause       : Clause,
+                            srcInfo      : Option[SourceInfo],
+                            propertyType : properties.Property)
+  : CCAssertionClause = {
+    val richClause = new CCAssertionClause(clause, srcInfo, propertyType)
+    clauseToRichClause += clause -> richClause
     richClause
   }
 
@@ -376,7 +405,7 @@ class CCReader private (prog : Program,
   private val processes =
     new ArrayBuffer[(ParametricEncoder.Process, ParametricEncoder.Replication)]
 
-  private val assertionClauses = new ArrayBuffer[CCClause]
+  private val assertionClauses = new ArrayBuffer[CCAssertionClause]
   private val timeInvariants = new ArrayBuffer[Clause]
 
   private val clauses =
@@ -442,7 +471,8 @@ class CCReader private (prog : Program,
                     " in one step")
                 val newAssertionClause = merge(c.clause, currentClause.clause)
                 if (!newAssertionClause.hasUnsatConstraint)
-                  assertionClauses += addRichClause(newAssertionClause, c.srcInfo)
+                  assertionClauses += mkRichAssertionClause(
+                    newAssertionClause, c.srcInfo, c.property)
               }
           }
           case None =>
@@ -529,10 +559,10 @@ class CCReader private (prog : Program,
   //////////////////////////////////////////////////////////////////////////////
 
   if (useTime) {
-    globalVars addVar GT
-    globalVars.inits += CCTerm(GT.term, CCClock, None)
-    globalVars addVar GTU
-    globalVars.inits += CCTerm(GTU.term, CCInt, None)
+    GlobalVars addVar GT
+    GlobalVars.inits += CCTerm(GT.term, CCClock, None)
+    GlobalVars addVar GTU
+    GlobalVars.inits += CCTerm(GTU.term, CCInt, None)
     variableHints += List()
     variableHints += List()
   }
@@ -655,9 +685,21 @@ class CCReader private (prog : Program,
   val heapTerm = heapVar.term
 
   if (modelHeap) {
-    globalVars addVar heapVar
+    GlobalVars addVar heapVar
+    GlobalVars.inits += CCTerm(heap.emptyHeap(), CCHeap(heap), None)
+    variableHints += List()
+  }
 
-    globalVars.inits += CCTerm(heap.emptyHeap(), CCHeap(heap), None)
+  /**
+   * For checking [[properties.MemValidCleanup]], a prophecy variable is used.
+   */
+  private val memCleanupProphecyVar =
+    new CCVar("@v_cleanup", None, CCHeapPointer(heap, CCVoid))
+  if ((propertiesToCheck contains properties.MemValidCleanup) ||
+      propertiesToCheck.contains(properties.MemValidTrack) &&
+       TriCeraParameters.get.useMemCleanupForMemTrack) {
+    GlobalVars addVar memCleanupProphecyVar
+    GlobalVars.inits += CCTerm(heap.nullAddr(), memCleanupProphecyVar.typ, None)
     variableHints += List()
   }
 
@@ -743,16 +785,22 @@ class CCReader private (prog : Program,
           // nothing
       }
 
-    // prevent time variables and heap variable from being initialised twice
-    globalVars.inits ++= (globalVarSymex.getValues drop
-      (if (modelHeap) 1 else 0) + (if (useTime) 2 else 0))
+    // prevent time variables, heap variable, and global ghost variables
+    // from being initialised twice
+    // TODO: This is very brittle and unintuitive - come up with a better solution.
+    GlobalVars.inits ++= (globalVarSymex.getValues drop
+      (if (modelHeap) 1 else 0) + (if (useTime) 2 else 0) +
+      (if ((propertiesToCheck contains properties.MemValidCleanup) ||
+           propertiesToCheck.contains(properties.MemValidTrack) &&
+           TriCeraParameters.get.useMemCleanupForMemTrack) 1 else 0))
     // if while adding glboal variables we have changed the heap, the heap term
     // needs to be reinitialised as well. Happens with global array allocations.
     if (modelHeap) {
-      val initialisedHeapValue = globalVarSymex.getValues.head
-      val initialHeapValue = IConstant(globalVars.vars.head.term)
+      val heapInd = GlobalVars.lastIndexWhere(heapVar)
+      val initialisedHeapValue = globalVarSymex.getValues(heapInd)
+      val initialHeapValue = IConstant(GlobalVars.vars(heapInd).term)
       if (modelHeap && initialisedHeapValue.toTerm != initialHeapValue) {
-        globalVars.inits(0) = initialisedHeapValue
+        GlobalVars.inits(heapInd) = initialisedHeapValue
       }
     }
 
@@ -789,9 +837,9 @@ class CCReader private (prog : Program,
 
     for(fun <- contractFuns ++ funsThatMightHaveACSLContracts.keys) {
       val funDef = FuncDef(fun.function_def_)
-      localVars.pushFrame
+      LocalVars.pushFrame
       pushArguments(fun.function_def_)
-      val functionParams = localVars getVarsInTopFrame
+      val functionParams = LocalVars getVarsInTopFrame
 
       val oldVars = allFormalVars map (v =>
         new CCVar(v.name + "_old", v.srcInfo, v.typ))
@@ -802,7 +850,7 @@ class CCReader private (prog : Program,
       // the post-condition: f_post(oldVars, postGlobalVars, postResVar)
       // we first pass all current vars in context as old vars (oldVars)
       // then we pass all effected output vars (which are globals + resVar)
-      val postGlobalVars = globalVars.vars map (v =>
+      val postGlobalVars = GlobalVars.vars map (v =>
         new CCVar(v.name + "_post", v.srcInfo, v.typ))
       val postResVar = getType(fun.function_def_) match {
         case CCVoid => None
@@ -815,17 +863,18 @@ class CCReader private (prog : Program,
       val prePredArgACSLNames = allFormalVars map (_.name)
       val postPredACSLArgNames =
         allFormalVars.map(v => "\\old(" + v.name + ")") ++
-        globalVars.vars.map(v => v.name) ++ Seq("\\result")
+        GlobalVars.vars.map(v => v.name) ++
+        (if(postResVar nonEmpty) Seq("\\result") else Nil)
 
       val postOldVarsMap: Map[String, CCVar] =
       (allFormalVars.map(_ name) zip oldVars).toMap
       val postGlobalVarsMap: Map[String, CCVar] =
-        (globalVars.vars.map(_ name) zip postGlobalVars).toMap
+        (GlobalVars.vars.map(_ name) zip postGlobalVars).toMap
 
       val postPred = newPred(funDef.name + "_post", postVars,
         Some(getSourceInfo(fun))) // todo: end line of fun?
 
-      localVars.popFrame
+      LocalVars.popFrame
 
       class ReaderFunctionContext extends ACSLTranslator.FunctionContext {
         def getOldVar(ident: String): Option[CCVar] =
@@ -836,7 +885,7 @@ class CCReader private (prog : Program,
 
         def getParams: Seq[CCVar] = functionParams
 
-        def getGlobals: Seq[CCVar] = globalVars.vars - heapVar
+        def getGlobals: Seq[CCVar] = GlobalVars.vars - heapVar
 
         def getResultVar: Option[CCVar] = postResVar
 
@@ -913,12 +962,12 @@ class CCReader private (prog : Program,
       val (prePred, postPred) = (funContext.prePred, funContext.postPred)
       setPrefix(name)
 
-      localVars.pushFrame
+      LocalVars.pushFrame
       val stm = pushArguments(f.function_def_)
 
       val prePredArgs = allFormalVarTerms.toList
 
-      for (v <- functionPostOldArgs(name)) localVars addVar v
+      for (v <- functionPostOldArgs(name)) LocalVars addVar v
 
       val entryPred = newPred(Nil, Some(getSourceInfo(f)))
 
@@ -940,7 +989,7 @@ class CCReader private (prog : Program,
 
       functionExitPreds += ((name, finalPred))
 
-      val globalVarTerms : Seq[ITerm] = globalVars.formalVarTerms
+      val globalVarTerms : Seq[ITerm] = GlobalVars.formalVarTerms
       val postArgs : Seq[ITerm] = (allFormalVarTerms drop prePredArgs.size) ++
         globalVarTerms ++ resVar.map(v => IConstant(v.term))
 
@@ -964,7 +1013,7 @@ class CCReader private (prog : Program,
       clauses.clear
       assertionClauses.clear
 
-      localVars popFrame
+      LocalVars popFrame
     }
 
     // then translate the threads
@@ -984,17 +1033,17 @@ class CCReader private (prog : Program,
             }
             case thread : ParaThread => {
               setPrefix(thread.cident_2)
-              localVars pushFrame
+              LocalVars pushFrame
               val threadVar = new CCVar(thread.cident_1,
                 Some(getSourceInfo(thread)),
                 CCInt)
-              localVars addVar threadVar
+              LocalVars addVar threadVar
               val translator = FunctionTranslator.apply
               val finalPred = translator translateNoReturn(thread.compound_stm_)
               functionExitPreds += ((thread.cident_2, finalPred))
               processes += ((clauses.toList, ParametricEncoder.Infinite))
               clauses.clear
-              localVars popFrame
+              LocalVars popFrame
             }
           }
 
@@ -1017,7 +1066,7 @@ class CCReader private (prog : Program,
         case Some(funDef) => {
           setPrefix(entryFunction)
 
-          localVars pushFrame
+          LocalVars pushFrame
 
           val f = FuncDef(funDef)
 
@@ -1044,40 +1093,48 @@ class CCReader private (prog : Program,
 
           functionExitPreds += ((f.name, finalPred))
 
-          // add an assertion to track memory safety (i.e., no memory leaks)
-          // currently this is only added to the exit point of the entry function,
-          if (modelHeap && trackMemorySafety) {
+          /**
+           * Add an assertion that all pointers that are in scope at the
+           * exit of `entryFunction` are freed using the prophecy variable.
+           * This ensures [[properties.MemValidCleanup]].
+          */
+          if (modelHeap &&
+              ((propertiesToCheck contains properties.MemValidCleanup) ||
+               propertiesToCheck.contains(properties.MemValidTrack) &&
+               TriCeraParameters.get.useMemCleanupForMemTrack)) {
+            val heapInd = GlobalVars.lastIndexWhere(heapVar)
+            val cleanupVarInd = GlobalVars.lastIndexWhere(memCleanupProphecyVar)
+
+            if (heapInd == -1 || cleanupVarInd == -1) {
+              assert(false, "Could not find the heap term or the mem-cleanup" +
+                            "prophecy variable term!")
+            }
+
             import HornClauses._
             import IExpression._
             finalPred match {
-              case CCPredicate(_, args, _) if args.head.sort == heap.HeapSort =>
-                // passing sort as CCVoid as it is not important
-                val addrVar = getFreshEvalVar(CCHeapPointer(heap, CCVoid), None)  // todo: add proper line numbers for auto-added free assertions
+              case CCPredicate(_, args, _)
+                if args(heapInd).sort == heap.HeapSort &&
+                   args(cleanupVarInd).sort == heap.AddressSort =>
+
                 val resVar = getResVar(args.last.typ)
-                var excludedAddresses = i(true)
-                for (arg <- args) arg.typ match {
-                  case arr: CCHeapArrayPointer
-                    if arr.arrayLocation == ArrayLocation.Global =>
-                    excludedAddresses = excludedAddresses &&&
-                      !heap.within(arg.term, addrVar.term)
-                  case _                                         => // nothing
-                }
                 assertionClauses +=
-                  addRichClause(((heap.read(args.head.term, addrVar.term) === defObj()) :-
-                    (atom(finalPred,
-                       allFormalVarTerms.toList ++
-                       resVar.map(v => IConstant(v.term)) take finalPred.arity)
-                     &&& excludedAddresses)),
-                    None) // todo: add proper line numbers for auto-added free assertions
-              case _ => throw new TranslationException("Tried to add -memtrack" +
-                "assertion but could not find the heap term!")
+                mkRichAssertionClause(
+                    (args(cleanupVarInd).term === heap.nullAddr()) :-
+                     atom(finalPred,
+                          allFormalVarTerms.toList ++
+                          resVar.map(v => IConstant(v.term)) take finalPred.arity),
+                    None, properties.MemValidCleanup)
+              case _ =>
+                assert(false, s"$finalPred does not contain the heap variable or" +
+                              s"the memory cleanup prophecy variable!")
             }
           }
 
           processes += ((clauses.toList, ParametricEncoder.Singleton))
           clauses.clear
 
-          localVars popFrame
+          LocalVars popFrame
         }
         case None =>
           warn("entry function \"" + entryFunction + "\" not found")
@@ -1405,11 +1462,12 @@ class CCReader private (prog : Program,
                             "size specified in an intialized array expression!")
                       }
                       import IExpression._
+                      val heapInd = GlobalVars.lastIndexWhere(heapVar)
                       val initHeapTerm =
-                        if (values.getValues.head.toTerm == IConstant(heapTerm)) {
-                          CCTerm(globalVars.inits.head.toTerm, CCHeap(heap), srcInfo)
+                        if (values.getValues(heapInd).toTerm == IConstant(heapTerm)) {
+                          CCTerm(GlobalVars.inits(heapInd).toTerm, CCHeap(heap), srcInfo)
                         } else
-                          CCTerm(values.getValues.head.toTerm, CCHeap(heap), srcInfo)
+                          CCTerm(values.getValues(heapInd).toTerm, CCHeap(heap), srcInfo)
                       val objTerm = CCTerm(arrayPtr.elementType.getZeroInit,
                         arrayPtr.elementType, srcInfo)
                       val arrayTerm =
@@ -1448,11 +1506,12 @@ class CCReader private (prog : Program,
                   val objValue = if (global) typ.elementType.getZeroInit
                   else typ.elementType.getNonDet
                   val objTerm = CCTerm(objValue, typ.elementType, srcInfo)
+                  val heapInd = GlobalVars.lastIndexWhere(heapVar)
                   val initHeapTerm =
-                    if (values.getValues.head.toTerm == IConstant(heapTerm)) {
-                      CCTerm(globalVars.inits.head.toTerm, CCHeap(heap), srcInfo)
+                    if (values.getValues(heapInd).toTerm == IConstant(heapTerm)) {
+                      CCTerm(GlobalVars.inits(heapInd).toTerm, CCHeap(heap), srcInfo)
                     } else
-                      CCTerm(values.getValues.head.toTerm, CCHeap(heap), srcInfo)
+                      CCTerm(values.getValues(heapInd).toTerm, CCHeap(heap), srcInfo)
                   val addressRangeValue = varDec.initArrayExpr match {
                     case Some(expr) =>
                       val arraySize =
@@ -1475,10 +1534,10 @@ class CCReader private (prog : Program,
         // do not use actualType below, take from lhsVar
 
         if (global) {
-          globalVars addVar actualLhsVar
+          GlobalVars addVar actualLhsVar
           variableHints += List()
         } else {
-          localVars addVar actualLhsVar
+          LocalVars addVar actualLhsVar
         }
 
         actualLhsVar.typ match {
@@ -1528,7 +1587,7 @@ class CCReader private (prog : Program,
                 new CCVar(name, Some(getSourceInfo(predExp)), typ)
             }
             values.saveState
-            ccVars.foreach(localVars addVar)
+            ccVars.foreach(LocalVars addVar)
             for ((ccVar, ind) <- ccVars.zipWithIndex) {
               values.addValue(CCTerm(IExpression.v(ind), ccVar.typ, ccVar.srcInfo))
             }
@@ -1558,7 +1617,7 @@ class CCReader private (prog : Program,
 
             val subst =
               (for ((v, n) <-
-                      (globalVars.iterator ++ localVars.iterator).zipWithIndex)
+                      (GlobalVars.iterator ++ LocalVars.iterator).zipWithIndex)
                yield (v.term.asInstanceOf[ConstantTerm] -> IExpression.v(n))).toMap
 
       import AnnotationParser._
@@ -1889,14 +1948,14 @@ class CCReader private (prog : Program,
       var enumerators = new MHashMap[String, IdealInt]
       val symex = Symex(null) // a temporary Symex to collect enum declarations
       // to deal with fields referring to same-enum fields, e.g. enum{a, b = a+1}
-      localVars pushFrame // we also need to add them as vars
+      LocalVars pushFrame // we also need to add them as vars
 
       for (s <- specs) s match {
         case s : Plain => {
           val ind = nextInd
           nextInd = nextInd + 1
           val v = new CCVar(s.cident_, Some(getSourceInfo(s)), CCInt)
-          localVars addVar v
+          LocalVars addVar v
           symex.addValue(CCTerm(IIntLit(ind), CCInt, v.srcInfo))
           enumerators += ((s.cident_, ind))
         }
@@ -1912,13 +1971,13 @@ class CCReader private (prog : Program,
           nextInd = ind + 1
           val v = new CCVar(s.cident_,
             Some(getSourceInfo(s)), CCInt)
-          localVars addVar v
+          LocalVars addVar v
           symex.addValue(CCTerm(IIntLit(ind), CCInt, v.srcInfo))
           enumerators += ((s.cident_, ind))
         }
       }
 
-      localVars popFrame
+      LocalVars popFrame
 
       val newEnum = CCIntEnum(enumName, enumerators.toSeq)
       enumDefs.put(enumName, newEnum)
@@ -2090,19 +2149,23 @@ class CCReader private (prog : Program,
 
     //todo:Heap get rid of this or change name
     def heapRead(ptrExpr : CCExpr, assertMemSafety : Boolean = true,
-                 assumeMemSafety : Boolean = true) : CCTerm = {
+                 assumeMemSafety : Boolean = true)
+    : CCTerm = {
       val (objectGetter, typ : CCType) = ptrExpr.typ match {
         case typ : CCHeapPointer => (sortGetterMap(typ.typ.toSort), typ.typ)
         case _ => throw new TranslationException(
           "Can only read from heap pointers! (" + ptrExpr + ")")
       }
       val readObj = heap.read(getValue(heapTermName).toTerm, ptrExpr.toTerm)
-      if (assertMemSafety)
-        assertProperty(heap.heapADTs.hasCtor(readObj, sortCtorIdMap(typ.toSort)),
-          ptrExpr.srcInfo) // todo: add tester methods for user ADT sorts?
-      // also add memory safety assumptions to the clause
-      if (assertMemSafety && assumeMemSafety)
-        addGuard(heap.heapADTs.hasCtor(readObj, sortCtorIdMap(typ.toSort)))
+      if (assertMemSafety && propertiesToCheck.contains(properties.MemValidDeref)) {
+        assertProperty(
+          heap.heapADTs.hasCtor(readObj, sortCtorIdMap(typ.toSort)),
+          ptrExpr.srcInfo, properties.MemValidDeref)
+        // todo: add tester methods for user ADT sorts?
+        // also add memory safety assumptions to the clause
+        if (assumeMemSafety)
+          addGuard(heap.heapADTs.hasCtor(readObj, sortCtorIdMap(typ.toSort)))
+      }
       CCTerm(objectGetter(readObj), typ, ptrExpr.srcInfo)
     }
     def heapAlloc(value : CCTerm) : CCTerm = {
@@ -2135,8 +2198,10 @@ class CCReader private (prog : Program,
       val readAddress = CCTerm(heap.nth(arrExpr.toTerm, index.toTerm),
         CCHeapPointer(heap, arrType.elementType), arrExpr.srcInfo)
       val readValue = heapRead(readAddress, assertMemSafety, assumeMemSafety)
-      if (assertIndexWithinBounds)
-        assertProperty(heap.within(arrExpr.toTerm, readAddress.toTerm), arrExpr.srcInfo)
+      if (assertIndexWithinBounds &&
+          propertiesToCheck.contains(properties.MemValidDeref))
+        assertProperty(heap.within(arrExpr.toTerm, readAddress.toTerm),
+                       arrExpr.srcInfo, properties.MemValidDeref)
       readValue
     }
 
@@ -2153,7 +2218,8 @@ class CCReader private (prog : Program,
                   assumeMemSafety : Boolean = false) = {
       val newHeap = heap.writeADT(lhs, rhs.toTerm).asInstanceOf[IFunApp]
       setValue(heapTerm.name, CCTerm(newHeap, CCHeap(heap), rhs.srcInfo))
-      if (assertMemSafety) {
+      if (assertMemSafety &&
+          propertiesToCheck.contains(properties.MemValidDeref)) {
         def getObjAndSort(f : IFunApp) : (IFunApp, Sort) = {
           if (objectGetters contains f.fun) {
             val sort = f.fun.asInstanceOf[MonoSortedIFunction].resSort
@@ -2168,7 +2234,8 @@ class CCReader private (prog : Program,
         val (writtenObj, sort) = getObjAndSort(lhs)
 
         assertProperty(heap.heapADTs.hasCtor(writtenObj, sortCtorIdMap(sort)),
-          rhs.srcInfo) // todo: add tester methods for user ADT sorts?
+          rhs.srcInfo, properties.MemValidDeref)
+        // todo: add tester methods for user ADT sorts?
         // also add memory safety assumptions to the clause
         if (assumeMemSafety)
           addGuard(heap.heapADTs.hasCtor(writtenObj, sortCtorIdMap(sort)))
@@ -2190,18 +2257,50 @@ class CCReader private (prog : Program,
       setValue(heapTerm.name, CCTerm(newHeap, CCHeap(heap), None)) // todo: src info?
     }
 
-    def heapFree(t : CCExpr) = {
+    /**
+     * `free` is encoded by writing [[defObj]] to the pointed location.
+     */
+    def heapFree(t : CCExpr, srcInfo : Option[SourceInfo]) = {
       t.typ match {
         case p : CCHeapPointer =>
           val termToFree : IFunApp =
             heapRead(t, assertMemSafety = false).toTerm match {
-              case IFunApp(f, Seq(arg)) if (objectGetters contains f) &
+              case IFunApp(f, Seq(arg))  if (objectGetters contains f) &
                 arg.isInstanceOf[IFunApp] =>
                 arg.asInstanceOf[IFunApp]
               case _ => throw new TranslationException("Could not resolve" +
                 " the term to free: " + t)
             }
-          heapWrite(termToFree, CCTerm(p.heap._defObj, p, t.srcInfo))
+          if(propertiesToCheck contains properties.MemValidFree){
+            /**
+             * Add an assertion that `ptrExpr` is safe to free.
+             * Checking [[Heap.isAlloc]] is not sufficient: freed locations are
+             * marked by writing the default object to them, so we need to check
+             * that read(h, p) =/= defObj. A free is also valid when
+             * p is nullAddr.
+             */
+            val readObj = heap.read(
+              getValue(heapTermName).toTerm, t.toTerm)
+            assertProperty(t.toTerm === heap.nullAddr() |||
+                           readObj =/= heap._defObj,
+                           srcInfo, properties.MemValidFree)
+          }
+          if ((propertiesToCheck contains properties.MemValidCleanup) ||
+              propertiesToCheck.contains(properties.MemValidTrack) &&
+              TriCeraParameters.get.useMemCleanupForMemTrack) {
+            /**
+             * Set [[memCleanupProphecyVar]] back to NULL, if the freed address
+             * is the same as the one stored.
+             */
+            val prophInd = GlobalVars.lastIndexWhere(memCleanupProphecyVar)
+            val prophOldVal = getValues(prophInd).toTerm
+            setValue(prophInd, CCTerm(
+              IExpression.ite(prophOldVal === t.toTerm,
+                              heap.nullAddr(),
+                              prophOldVal), memCleanupProphecyVar.typ, None),
+                     false)
+          }
+          heapWrite(termToFree, CCTerm(p.heap._defObj, p, srcInfo))
         case p : CCHeapArrayPointer =>
           import IExpression._
           //val n = getFreshEvalVar(CCUInt)
@@ -2219,11 +2318,53 @@ class CCReader private (prog : Program,
             }
           heapWrite(termToFree, CCTerm(p.heap._defObj, p))*/
           // todo: what about ADTs?
-          //if(p.arrayType != HeapArray) throw new TranslationException("Trying to free global or stack pointer " + p)
-          // todo: unsafe instead of exception?
+          if (propertiesToCheck contains properties.MemValidFree) {
+            p.arrayLocation match {
+              case ArrayLocation.Heap =>
+                /**
+                 * Assert that either `t` is `null`, or
+                 * forall ind. t[ind] =/= defObj
+                 * (or equivalently forall ind. read(h, nth(t, ind)) =/= defObj)
+                 */
+                val ind      = getFreshEvalVar(CCInt, t.srcInfo)
+                val readAddr = heap.nth(t.toTerm, ind.term)
+                val readObj  = heap.read(getValue(heapTermName).toTerm,
+                                         readAddr)
+                assertProperty(t.toTerm === heap.nullAddr() |||
+                               (heap.within(t.toTerm, readAddr) ==>
+                                (readObj =/= heap._defObj)),
+                               srcInfo, properties.MemValidFree)
+              case _ =>
+                /**
+                 * Freeing non-heap memory is undefined behaviour.
+                 */
+                assertProperty(IExpression.i(false),
+                               srcInfo, properties.MemValidFree)
+            }
+          }
+          if ((propertiesToCheck contains properties.MemValidCleanup) ||
+              propertiesToCheck.contains(properties.MemValidTrack) &&
+              TriCeraParameters.get.useMemCleanupForMemTrack) {
+            /**
+             * Set [[memCleanupProphecyVar]] back to NULL, if the beginning of
+             * the freed address block is the same as the one stored.
+             */
+            val prophInd    = GlobalVars.lastIndexWhere(memCleanupProphecyVar)
+            val prophOldVal = getValues(prophInd).toTerm
+            setValue(prophInd, CCTerm(
+              IExpression.ite(prophOldVal === heap.nth(t.toTerm, 0),
+                              heap.nullAddr(),
+                              prophOldVal), memCleanupProphecyVar.typ, None),
+                     false)
+          }
           heapBatchWrite(getValue(heapTermName).toTerm, t.toTerm, defObj())
-        case _ => throw new TranslationException("Unsupported operation: " +
-          "trying to free " + t + ".")
+        case _ =>
+          /**
+           * Freeing a non-heap pointer.
+           */
+          if (propertiesToCheck contains properties.MemValidFree)
+            assertProperty(IExpression.i(false),
+                           srcInfo, properties.MemValidFree)
       }
     }
 
@@ -2244,7 +2385,7 @@ class CCReader private (prog : Program,
       initAtom = oldAtom
       values.clear
       oldValues copyToBuffer values
-      localVars.pop(localVars.size - values.size + globalVars.size)
+      LocalVars.pop(LocalVars.size - values.size + GlobalVars.size)
       guard = oldGuard
       touchedGlobalState = oldTouched
     }
@@ -2268,7 +2409,7 @@ class CCReader private (prog : Program,
       val freshVar = getFreshEvalVar(v.typ, v.srcInfo, varName)
       addValue(v)
       // reserve a local variable, in case we need one later
-      localVars addVar freshVar
+      LocalVars addVar freshVar
 
       if (usingInitialPredicates) {
         // if the pushed value refers to other variables,
@@ -2299,7 +2440,7 @@ class CCReader private (prog : Program,
 
     private def pushFormalVal(typ : CCType, srcInfo : Option[SourceInfo]) = {
       val freshVar = getFreshEvalVar(typ, srcInfo)
-      localVars addVar freshVar
+      LocalVars addVar freshVar
       addValue(CCTerm(freshVar.term, typ, srcInfo))
       addGuard(freshVar rangePred)
     }
@@ -2307,13 +2448,13 @@ class CCReader private (prog : Program,
     private def popVal = {
       val res = values.last
       values trimEnd 1
-      localVars.pop(1)
+      LocalVars.pop(1)
       res
     }
     private def topVal = values.last
     private def removeVal(ind : Int) {
       values.remove(ind)
-      localVars.remove(ind - globalVars.size)
+      LocalVars.remove(ind - GlobalVars.size)
     }
 
     private def outputClause(srcInfo : Option[SourceInfo]) : Unit =
@@ -2367,11 +2508,12 @@ class CCReader private (prog : Program,
       outputClause(elsePred, srcInfo)
     }
 
-    def assertProperty(property : IFormula,
-                       srcInfo : Option[SourceInfo]) : Unit = {
+    def assertProperty(property     : IFormula,
+                       srcInfo      : Option[SourceInfo],
+                       propertyType : properties.Property) : Unit = {
       import HornClauses._
       val clause = (property :- (initAtom &&& guard))
-      assertionClauses += addRichClause(clause, srcInfo)
+      assertionClauses += mkRichAssertionClause(clause, srcInfo, propertyType)
     }
 
     def addValue(t : CCExpr) = {
@@ -2435,12 +2577,12 @@ class CCReader private (prog : Program,
         ind
       }*/
       touchedGlobalState =
-        touchedGlobalState || actualInd < globalVars.size || !freeFromGlobal(t)
+        touchedGlobalState || actualInd < GlobalVars.size || !freeFromGlobal(t)
     }
 
     private def getVar (ind : Int) : CCVar = {
-      if (ind < globalVars.size) globalVars.vars(ind)
-      else localVars.vars(ind - globalVars.size)
+      if (ind < GlobalVars.size) GlobalVars.vars(ind)
+      else LocalVars.vars(ind - GlobalVars.size)
     }
     private def getVar (name : String) : CCVar = {
       val ind = lookupVar(name)
@@ -2882,9 +3024,9 @@ class CCReader private (prog : Program,
           restoreState
           addGuard(~cond)
           evalHelp(exp.exp_3)
-          localVars.update(localVars.size - 1,
+          LocalVars.update(LocalVars.size - 1,
             new CCVar(s"ite_${srcInfo.get.line}_${srcInfo.get.col}",
-                      localVars.last.srcInfo, localVars.last.typ))
+                      LocalVars.last.srcInfo, LocalVars.last.typ))
           outputClause(intermediatePred, srcInfo)
         }
       case exp : Elor =>
@@ -3068,7 +3210,7 @@ class CCReader private (prog : Program,
                   //newTerm
                   throw new TranslationException(
                     "Function contracts are currently not supported together " +
-                    s"with stack pointers (at ${exp.line_num}:${exp.col_num})")
+                    s"with stack pointers (${exp.line_num}:${exp.col_num})")
                 } else {
                   val ind = values.indexWhere(v => v == topVal)
                   assert(ind > -1 && ind < values.size - 1) // todo
@@ -3106,41 +3248,42 @@ class CCReader private (prog : Program,
         val srcInfo = Some(getSourceInfo(exp))
         // inline the called function
         printer print exp.exp_ match {
-          case "__VERIFIER_error" | "reach_error" => {
-            assertProperty(false, srcInfo)
+          case "reach_error" =>
+            /**
+             * A special SV-COMP function used in the unreach-call category.
+             * We directly rewrite this as `assert(0)`.
+             */
+            if(propertiesToCheck contains properties.Reachability)
+              assertProperty(false, srcInfo, properties.Reachability)
             pushVal(CCFormula(true, CCInt, srcInfo))
-          }
-          case name => {
+          case name =>
             outputClause(srcInfo)
             handleFunction(name, initPred, 0)
-          }
         }
 
       case exp : Efunkpar =>
         val srcInfo = Some(getSourceInfo(exp))
         (printer print exp.exp_) match {
-          case "assert" | "static_assert" | "__VERIFIER_assert"
-                          if (exp.listexp_.size == 1) =>
-          val property = exp.listexp_.head match {
-            case a : Efunkpar
-              if uninterpPredDecls contains (printer print a.exp_)      =>
-              val args = a.listexp_.map(atomicEval).map(_.toTerm)
-              val pred = uninterpPredDecls(printer print a.exp_)
-              atom(pred, args)
-            case interpPred : Efunkpar
-              if interpPredDefs contains(printer print interpPred.exp_) =>
-              val args = interpPred.listexp_.map (atomicEval).map (_.toTerm)
-              val formula = interpPredDefs (printer print interpPred.exp_)
-              // the formula refers to pred arguments as IVariable(index)
-              // we need to subsitute those for the actual arguments
-              VariableSubstVisitor (formula.f, (args.toList, 0) )
-            case _ =>
-              atomicEvalFormula(exp.listexp_.head).f
-          }
-          assertProperty(property, srcInfo)
-          pushVal(CCFormula(true, CCInt, srcInfo))
-        case "assume" | "__VERIFIER_assume"
-                          if (exp.listexp_.size == 1) =>
+          case "assert" | "static_assert" if exp.listexp_.size == 1 =>
+            val property = exp.listexp_.head match {
+              case a : Efunkpar
+                if uninterpPredDecls contains(printer print a.exp_) =>
+                val args = a.listexp_.map(atomicEval).map(_.toTerm)
+                val pred = uninterpPredDecls(printer print a.exp_)
+                atom(pred, args)
+              case interpPred : Efunkpar
+                if interpPredDefs contains(printer print interpPred.exp_) =>
+                val args    = interpPred.listexp_.map(atomicEval).map(_.toTerm)
+                val formula = interpPredDefs(printer print interpPred.exp_)
+                // the formula refers to pred arguments as IVariable(index)
+                // we need to subsitute those for the actual arguments
+                VariableSubstVisitor(formula.f, (args.toList, 0))
+              case _ =>
+                atomicEvalFormula(exp.listexp_.head).f
+            }
+            assertProperty(property, srcInfo, properties.UserAssertion)
+            pushVal(CCFormula(true, CCInt, srcInfo))
+        case "assume" if (exp.listexp_.size == 1) =>
           val property = exp.listexp_.head match {
             case a : Efunkpar
               if uninterpPredDecls contains(printer print a.exp_) =>
@@ -3197,7 +3340,7 @@ class CCReader private (prog : Program,
               "Unsupported alloc expression: " + (printer print exp))
           }
 
-          val arrayType = name match {
+          val arrayLoc = name match {
             case "malloc" | "calloc"           => ArrayLocation.Heap
             case "alloca" | "__builtin_alloca" => ArrayLocation.Stack
           }
@@ -3208,18 +3351,80 @@ class CCReader private (prog : Program,
 
           allocSize match {
             case CCTerm(IIntLit(IdealInt(1)), typ, srcInfo)
-              if typ.isInstanceOf[CCArithType] && !lhsIsArrayPointer =>
-              pushVal(heapAlloc(objectTerm))
+              if typ.isInstanceOf[CCArithType] && !lhsIsArrayPointer
+                 && arrayLoc == ArrayLocation.Heap =>
+              /**
+               * global and stack arrays are allocated using CCHeapArrayPointer,
+               * because CCHeapPointer does not distinguish between different
+               * allocation types. This difference is needed for correctly
+               * checking memory properties (e.g., only heap allocated memory
+               * can be freed).
+               */
+              val allocatedAddr = heapAlloc(objectTerm)
+
+              if ((propertiesToCheck contains properties.MemValidCleanup) ||
+                  propertiesToCheck.contains(properties.MemValidTrack) &&
+                  TriCeraParameters.get.useMemCleanupForMemTrack) {
+                /**
+                 * Nondeterministically write the address to the prophecy
+                 * variable [[memCleanupProphecyVar]].
+                 * I.e., nondet ==> prophTerm = allocatedAddr
+                 */
+                val prophVarInd = GlobalVars.lastIndexWhere(memCleanupProphecyVar)
+                val nondetTerm = IConstant(
+                  getFreshEvalVar(CCBool, None, name = "nondet").term)
+                setValue(prophVarInd,
+                         CCTerm(
+                           IExpression.ite(
+                             nondetTerm === ADT.BoolADT.True,
+                             allocatedAddr.toTerm,
+                             getValues(prophVarInd).toTerm
+                             ), memCleanupProphecyVar.typ, None),
+                         isIndirection = false)
+              }
+
+              pushVal(allocatedAddr)
             case CCTerm(sizeExp, typ, srcInfo) if typ.isInstanceOf[CCArithType] =>
               val addressRangeValue = heapBatchAlloc(objectTerm, sizeExp)
-//              localVars.incrementLastFrame
-              // todo: values addGuard ?
-              pushVal(CCTerm(addressRangeValue, CCHeapArrayPointer(heap, typ, arrayType), srcInfo))
+              val allocatedBlock =
+                CCTerm(addressRangeValue,
+                       CCHeapArrayPointer(heap, typ, arrayLoc), srcInfo)
+
+              if (arrayLoc == ArrayLocation.Heap &&
+                  ((propertiesToCheck contains properties.MemValidCleanup) ||
+                   propertiesToCheck.contains(properties.MemValidTrack) &&
+                   TriCeraParameters.get.useMemCleanupForMemTrack)) {
+                /**
+                 * Nondeterministically write the address to the prophecy
+                 * variable [[memCleanupProphecyVar]]. Here a corner case to
+                 * consider is when sizeExp is not > 0, in which case no memory
+                 * is allocated, hence no need to change the value of the
+                 * prophecy variable.
+                 * I.e., (nondet & sizeExp > 0) ==> prophTerm = allocatedAddr
+                 */
+                val prophVarInd = GlobalVars.lastIndexWhere(memCleanupProphecyVar)
+                val nondetTerm  = IConstant(
+                  getFreshEvalVar(CCBool, None, name = "nondet").term)
+                setValue(prophVarInd,
+                         CCTerm(
+                           IExpression.ite(
+                             nondetTerm === ADT.BoolADT.True & sizeExp > 0,
+                             heap.nth(allocatedBlock.toTerm, 0),
+                             getValues(prophVarInd).toTerm
+                             ), memCleanupProphecyVar.typ, None),
+                         isIndirection = false)
+              }
+              pushVal(allocatedBlock)
             // case CCTerm(IIntLit(IdealInt(n)), CCInt) =>
                 // todo: optimise constant size allocations > 1?
           }
         case name@("malloc" | "calloc" | "alloca" | "__builtin_alloca")
           if TriCeraParameters.parameters.value.useArraysForHeap =>
+          /**
+           * @todo Support checking [[properties.MemValidCleanup]] when using
+           *       arrays to model heaps.
+           */
+
           val (typ, allocSize) = exp.listexp_(0) match {
             case exp : Ebytestype =>
               (getType(exp), CCTerm(IIntLit(IdealInt(1)), CCInt, srcInfo))
@@ -3264,12 +3469,12 @@ class CCReader private (prog : Program,
           if (!modelHeap)
             throw NeedsHeapModelException
           throw new TranslationException("realloc is not supported.")
-        case "free" => // todo: what about trying to free unallocated or already freed addresses?
+        case "free" =>
           if (!modelHeap)
             throw NeedsHeapModelException
-          val t = atomicEval(exp.listexp_.head)
-          heapFree(t)
-          pushVal(CCTerm(0, CCVoid, srcInfo)) // free returns no value, pushing dummy
+          val ptrExpr = atomicEval(exp.listexp_.head)
+          heapFree(ptrExpr, srcInfo)
+          pushVal(CCTerm(0, CCVoid, srcInfo)) // free returns no value, push dummy
         case name =>
           // then we inline the called function
 
@@ -3293,8 +3498,8 @@ class CCReader private (prog : Program,
               }
           }
           if(argNames nonEmpty) {
-            val evalVars = localVars.getVarsInTopFrame.takeRight(argCount)
-            localVars.pop(argCount) // remove those vars
+            val evalVars = LocalVars.getVarsInTopFrame.takeRight(argCount)
+            LocalVars.pop(argCount) // remove those vars
             assert(argNames.length == argCount && evalVars.length == argCount)
             val newVars = if (((assertionClauses.map(_.clause.constants) ++
               clauses.flatMap(_._1.constants)) intersect evalVars.map(_.term)).nonEmpty) {
@@ -3303,12 +3508,12 @@ class CCReader private (prog : Program,
             } else {
               for ((oldVar, argName) <- evalVars zip argNames) yield {
                 val uniqueArgName =
-                  if (localVars.vars.exists(v => v.name == argName)) name + "_" + argName
+                  if (LocalVars.vars.exists(v => v.name == argName)) name + "_" + argName
                   else argName
                 new CCVar(uniqueArgName, oldVar.srcInfo, oldVar.typ)
               }
             }
-            newVars.foreach(localVars addVar)
+            newVars.foreach(LocalVars addVar)
           }
           //////////////////////////////////////////////////////////////////////
 
@@ -3424,9 +3629,11 @@ class CCReader private (prog : Program,
             val readValue = CCTerm(array.arrayTheory.
               select(arrayTerm.toTerm, index.toTerm), array.elementType, srcInfo)
             array.sizeExpr match {
-              case Some(expr) =>
+              case Some(expr)
+                if propertiesToCheck contains properties.MemValidDeref =>
                 assertProperty((index.toTerm >= 0) &&&
-                  (index.toTerm < expr.toTerm), srcInfo)
+                  (index.toTerm < expr.toTerm), srcInfo,
+                               properties.MemValidDeref)
               case _ => // no safety assertion needed for mathematical arrays
             }
             pushVal(readValue)
@@ -3457,11 +3664,11 @@ class CCReader private (prog : Program,
             argTerms = popVal.toTerm :: argTerms
 
           val postGlobalVars : Seq[ITerm] = // todo : use ctx postglobal?
-            for (v <- globalVars.vars)
+            for (v <- GlobalVars.vars)
             yield IExpression.i(v.sort newConstant (v.name + "_post")) // todo: refactor
 
           val globals : Seq[ITerm] =
-            for (n <- 0 until globalVars.size)
+            for (n <- 0 until GlobalVars.size)
             yield getValue(n, false).toTerm
 
           val prePredArgs : Seq[ITerm] = globals ++ argTerms
@@ -3474,12 +3681,13 @@ class CCReader private (prog : Program,
           val preAtom  = ctx.prePred(prePredArgs)
           val postAtom = ctx.postPred(postPredArgs)
 
-          assertProperty(preAtom, None) // todo: mark pre atom assertions
+          assertProperty(preAtom, functionEntry.srcInfo,
+                         properties.FunctionPrecondition(name,functionEntry.srcInfo))
 
           addGuard(postAtom)
 
           for (((c, t), n) <- (postGlobalVars.iterator zip
-                                 globalVars.formalTypes.iterator).zipWithIndex)
+                                 GlobalVars.formalTypes.iterator).zipWithIndex)
             setValue(n, CCTerm(c, t, None), false) // todo: srcInfo?
 
           resVar match {
@@ -3492,7 +3700,6 @@ class CCReader private (prog : Program,
               //val argNames = PredPrintContextPrintContext.predArgNames(predDecl.pred)
               var argTerms : List[ITerm] = List()
               for (_ <- 0 until argCount) {
-                val argName =
                 argTerms = popVal.toTerm :: argTerms
               }
               pushVal(CCFormula(predDecl(argTerms), CCInt, None)) // todo:srcInfo
@@ -3634,7 +3841,7 @@ class CCReader private (prog : Program,
                              exit : CCPredicate,
                              args : List[CCType],
                              isNoReturn : Boolean) : Unit = {
-    localVars pushFrame
+    LocalVars pushFrame
     val stm = pushArguments(functionDef, args)
 
     // this might be an inlined function in an expression where we need to
@@ -3650,7 +3857,7 @@ class CCReader private (prog : Program,
       } else
         translator.translateWithReturn(stm, entry)
     functionExitPreds += ((FuncDef(functionDef).name, finalPred))
-    localVars popFrame
+    LocalVars popFrame
   }
 
   private def createHeapPointer(decl : BeginPointer, typ : CCType) :
@@ -3731,7 +3938,7 @@ class CCReader private (prog : Program,
               }
               val declaredVar =
                 new CCVar(name, Some(getSourceInfo(argDec)), actualType)
-              localVars addVar declaredVar
+              LocalVars addVar declaredVar
 
             case argDec : TypeHintAndParam =>
               val typ = getType(argDec.listdeclaration_specifier_)
@@ -3743,13 +3950,13 @@ class CCReader private (prog : Program,
               val declaredVar = new CCVar(getName(argDec.declarator_),
                                           Some(getSourceInfo(argDec)),
                                           actualType)
-              localVars addVar declaredVar
+              LocalVars addVar declaredVar
               processHints(argDec.listannotation_)
 //            case argDec : Abstract =>
           }
 //      case dec : OldFuncDef =>
 //        for (ident <- dec.listcident_)
-//          localVars += new ConstantTerm(ident)
+//          LocalVars += new ConstantTerm(ident)
       case dec : OldFuncDec =>
         // arguments are not specified ...
     }
@@ -3963,7 +4170,7 @@ class CCReader private (prog : Program,
               }
             }
 
-            override def getGlobals: Seq[CCVar] = globalVars.vars
+            override def getGlobals: Seq[CCVar] = GlobalVars.vars
             override def sortWrapper(s: Sort): Option[IFunction] =
               sortWrapperMap get s
             override def sortGetter(s: Sort): Option[IFunction] =
@@ -3978,7 +4185,8 @@ class CCReader private (prog : Program,
             override def getHeap: HeapObj =
               if (modelHeap) heap else throw NeedsHeapModelException
             override def getHeapTerm: ITerm =
-              if (modelHeap) stmSymex.getValues.head.toTerm
+              if (modelHeap)
+                stmSymex.getValues(GlobalVars.lastIndexWhere(heapVar)).toTerm
               else throw NeedsHeapModelException
             override def getOldHeapTerm: ITerm =
               getHeapTerm // todo: heap term for exit predicate?
@@ -3992,7 +4200,8 @@ class CCReader private (prog : Program,
             "/*@" + annot + "*/", new LocalContext()) match {
             case res: tricera.acsl.StatementAnnotation =>
               if (res.isAssert) {
-                stmSymex.assertProperty(res.f, Some(getSourceInfo(stm)))
+                stmSymex.assertProperty(res.f, Some(getSourceInfo(stm)),
+                                        properties.Reachability)
               } else
                 warn("Ignoring annotation: " + annot)
             case _ => warn("Ignoring annotation: " + annot)
@@ -4028,7 +4237,7 @@ class CCReader private (prog : Program,
               }
             }
 
-            override def getGlobals : Seq[CCVar] = globalVars.vars
+            override def getGlobals : Seq[CCVar] = GlobalVars.vars
             override def sortWrapper(s : Sort) : Option[IFunction] =
               sortWrapperMap get s
             override def sortGetter(s : Sort) : Option[IFunction] =
@@ -4043,7 +4252,8 @@ class CCReader private (prog : Program,
             override def getHeap : HeapObj =
               if (modelHeap) heap else throw NeedsHeapModelException
             override def getHeapTerm : ITerm =
-              if (modelHeap) stmSymex.getValues.head.toTerm
+              if (modelHeap)
+                stmSymex.getValues(GlobalVars.lastIndexWhere(heapVar)).toTerm
               else throw NeedsHeapModelException
             override def getOldHeapTerm : ITerm =
               getHeapTerm // todo: heap term for exit predicate?
@@ -4105,7 +4315,7 @@ class CCReader private (prog : Program,
           Some(getSourceInfo(compound)))
         )
       case compound : ScompTwo => {
-        localVars pushFrame
+        LocalVars pushFrame
 
         val stmsIt = ap.util.PeekIterator(compound.liststm_.iterator)
 
@@ -4127,9 +4337,8 @@ class CCReader private (prog : Program,
         }
         output(addRichClause(entryClause, entryPred.srcInfo))
 
-        translateStmSeq(stmsIt, entryPred, exit,
-                        freeArraysOnStack = trackMemorySafety && modelHeap)
-        localVars popFrame
+        translateStmSeq(stmsIt, entryPred, exit)
+        LocalVars popFrame
       }
     }
 
@@ -4183,19 +4392,17 @@ class CCReader private (prog : Program,
           Some(getSourceInfo(compound))))
       }
       case compound : ScompTwo => {
-        localVars pushFrame
+        LocalVars pushFrame
 
         val stmsIt = compound.liststm_.iterator
-        translateStmSeq(stmsIt, entry, exit,
-                        freeArraysOnStack = trackMemorySafety && modelHeap)
-        localVars popFrame
+        translateStmSeq(stmsIt, entry, exit)
+        LocalVars popFrame
       }
     }
 
     private def translateStmSeq(stmsIt : Iterator[Stm],
                                 entry : CCPredicate,
-                                exit : CCPredicate,
-                                freeArraysOnStack : Boolean = false) : Unit = {
+                                exit : CCPredicate) : Unit = {
       var prevPred = entry
       while (stmsIt.hasNext)
         stmsIt.next match {
@@ -4203,44 +4410,17 @@ class CCReader private (prog : Program,
             val srcInfo = Some(getSourceInfo(stm))
             prevPred = translate(stm.dec_, prevPred)
             if (!stmsIt.hasNext) {
-              if (freeArraysOnStack) {
-                // free stack allocated arrays that use the theory of heap
-                val freeSymex = Symex(prevPred)
-                for (v <- localVars.getVarsInTopFrame) v.typ match {
-                  case a : CCHeapArrayPointer
-                    if a.arrayLocation == ArrayLocation.Stack =>
-                    freeSymex.heapFree(CCTerm(v.term, v.typ, v.srcInfo))
-                    prevPred = newPred(Nil, None) // todo: line no?
-                    freeSymex.outputClause(prevPred, srcInfo)
-                  case _ => // nothing
-                }
-                freeSymex.outputClause(exit, srcInfo)
-              } else {
-                output(addRichClause(Clause(
-                  atom(exit, allFormalVarTerms take exit.arity),
-                  List(atom(prevPred, allFormalVarTerms take prevPred.arity)),
-                  true), srcInfo))
-              }
+              output(addRichClause(Clause(
+                atom(exit, allFormalVarTerms take exit.arity),
+                List(atom(prevPred, allFormalVarTerms take prevPred.arity)),
+                true), srcInfo))
             }
           }
           case stm => {
             val srcInfo = Some(getSourceInfo(stm))
-            var nextPred = if (stmsIt.hasNext || freeArraysOnStack) newPred(Nil, None) // todo: line no?
+            var nextPred = if (stmsIt.hasNext) newPred(Nil, None) // todo: line no?
                            else exit
             translate(stm, prevPred, nextPred)
-            if (freeArraysOnStack && !stmsIt.hasNext) {
-              // free stack allocated arrays that use the theory of heap
-              val freeSymex = Symex(nextPred)
-              for (v <- localVars.getVarsInTopFrame) v.typ match {
-                case a : CCHeapArrayPointer
-                  if a.arrayLocation == ArrayLocation.Stack =>
-                  freeSymex.heapFree(CCTerm(v.term, v.typ, v.srcInfo)) // todo: line no probably incorrect
-                  nextPred = newPred(Nil, v.srcInfo)  // todo: line no probably incorrect
-                  freeSymex.outputClause(nextPred, srcInfo)
-                case _ => // nothing
-              }
-              freeSymex.outputClause(exit, srcInfo)
-            }
             prevPred = nextPred
           }
         }
@@ -4427,7 +4607,9 @@ class CCReader private (prog : Program,
           case Seq() =>
             // add an assertion that we never try to jump to a case that
             // does not exist. TODO: add a parameter for this?
-            selectorSymex assertProperty(or(guards), Some(getSourceInfo(stm)))
+            selectorSymex assertProperty(
+              or(guards), Some(getSourceInfo(stm)),
+              properties.SwitchCaseValidJump)
           case Seq((_, target)) => {
             selectorSymex.saveState
             selectorSymex addGuard ~or(guards)
@@ -4449,7 +4631,7 @@ class CCReader private (prog : Program,
         jumpLocs += ((jump.cident_, entry, allFormalVarTerms, clauses.size,
           getSourceInfo(jump)))
         // reserve space for the later jump clause
-        output(CCClause(null, null))
+        output(new CCClause(null, null))
       }
       case jump : SjumpTwo => { // continue
         if (innermostLoopCont == null)
@@ -4467,18 +4649,6 @@ class CCReader private (prog : Program,
         returnPred match {
           case Some(rp) => {
             var nextPred = entry
-            if (modelHeap && trackMemorySafety) {
-              // free stack allocated arrays that use the theory of heap
-              val freeSymex = Symex(entry)
-              for (v <- localVars.getVarsInTopFrame) v.typ match {
-                case a : CCHeapArrayPointer
-                  if a.arrayLocation == ArrayLocation.Stack =>
-                  freeSymex.heapFree(CCTerm(v.term, v.typ, v.srcInfo)) // line no probably incorrect
-                  nextPred = newPred(Nil, srcInfo)
-                  freeSymex.outputClause(nextPred, srcInfo)
-                case _ => // nothing
-              }
-            }
             val args = allFormalVarTerms take rp.arity
             output(addRichClause(Clause(atom(rp, args),
                           List(atom(nextPred, allFormalVarTerms take nextPred.arity)),
@@ -4493,45 +4663,22 @@ class CCReader private (prog : Program,
         implicit val evalSettings = symex.EvalSettings.default
         val retValue = symex eval jump.exp_
         returnPred match {
-          case Some(rp) => {
-            if (modelHeap && trackMemorySafety) {
-              localVars.pushFrame
-              localVars.addVar(rp.argVars.last)
-              var nextPred = newPred(Nil, srcInfo)
-              val args = symex.getValuesAsTerms ++ List(retValue.toTerm)
-              symex outputClause(atom(nextPred, args take nextPred.arity), srcInfo) //output one clause in case return expr modifies heap
-              val freeSymex = Symex(nextPred) // reinitialise init atom
-              // free stack allocated arrays that use the theory of heap
-              for (v <- localVars.getVarsInTopFrame) v.typ match {
-                case a : CCHeapArrayPointer
-                  if a.arrayLocation == ArrayLocation.Stack =>
-                  freeSymex.heapFree(CCTerm(v.term, v.typ, v.srcInfo)) // todo: line no probably incorrect
-                  nextPred = newPred(Nil, srcInfo)
-                  freeSymex.outputClause(nextPred, srcInfo)
-                case _ => // nothing
-              }
-              val retArgs = (freeSymex.getValuesAsTerms take (rp.arity - 1)) ++
-                Seq(freeSymex.getValuesAsTerms.last)
-              freeSymex outputClause(atom(rp, retArgs), srcInfo)
-              localVars.popFrame
-            } else {
-              val args = (symex.getValuesAsTerms take (rp.arity - 1)) ++
-                List(retValue.toTerm)
-              symex outputClause(atom(rp, args), srcInfo)
-            }
-          }
+          case Some(rp) =>
+            val args = (symex.getValuesAsTerms take (rp.arity - 1)) ++
+                       List(retValue.toTerm)
+            symex outputClause(atom(rp, args), srcInfo)
           case None =>
             throw new TranslationException(
               "\"return\" can only be used within functions")
         }
       }
-      case _ : SjumpAbort | _ : SjumpExit => { // abort() or exit(int status)
-        output(addRichClause(Clause(atom(globalExitPred, Nil),
-                      List(atom(entry, allFormalVarTerms take entry.arity)),
-                      true), srcInfo))
+      case _ : SjumpAbort | _ : SjumpExit => // abort() or exit(int status)
+        output(addRichClause(
+          Clause(atom(globalExitPred, Nil),
+                 List(atom(entry, allFormalVarTerms take entry.arity)),
+                 true), srcInfo))
       }
     }
-    }
 
     private def translate(aStm : Atomic_stm,
                           entry : CCPredicate,
@@ -4613,7 +4760,7 @@ class CCReader private (prog : Program,
                              if (singleThreaded) {
                                if (useTime) 2 else 0 // todo : anything for heap here? why only 2 if useTime?
                              } else {
-                               globalVars.size
+                               GlobalVars.size
                              },
                              None,
                              if (useTime)
diff --git a/src/tricera/concurrency/ccreader/CCType.scala b/src/tricera/concurrency/ccreader/CCType.scala
index d857e0b..52bf75d 100644
--- a/src/tricera/concurrency/ccreader/CCType.scala
+++ b/src/tricera/concurrency/ccreader/CCType.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2023 Zafer Esen, Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2024 Zafer Esen, Philipp Ruemmer. All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -468,11 +468,11 @@ case class CCHeapPointer(heap: Heap, typ: CCType) extends CCPointer(typ) {
   override def toString: String = typ.shortName + " pointer to heap"
 }
 
-// arrays on the heap do not get automatically freed.
-// global arrays get automatically freed (as they are not really on the heap)
-//   when the main function returns.
-// "alloca" and stack arrays get automatically freed when the calling
-// function returns.
+/**
+ * `Heap`   : arrays allocated via memory allocation functions.
+ * `Stack`  : arrays declared on the stack, or allocated via `alloca`.
+ * `Global` : global arrays.
+ */
 object ArrayLocation extends Enumeration {
   type ArrayLocation = Value
   val Global, Stack, Heap = Value
diff --git a/src/tricera/params/TriCeraParameters.scala b/src/tricera/params/TriCeraParameters.scala
index 5c9b9dd..7034fab 100644
--- a/src/tricera/params/TriCeraParameters.scala
+++ b/src/tricera/params/TriCeraParameters.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2015-2023 Zafer Esen, Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2015-2024 Zafer Esen, Philipp Ruemmer. All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -59,7 +59,41 @@ class TriCeraParameters extends GlobalParameters {
 
   var showVarLineNumbersInTerms : Boolean = false
 
-  var shouldTrackMemory : Boolean = false
+  /**
+   * Properties that TriCera should check.
+   * Note that reach safety will be checked by default when no other properties
+   * are specified. If any other property is specified, reach safety is not
+   * checked unless explicitly specified.
+   */
+  var checkReachSafety : Boolean = false
+  var checkMemTrack    : Boolean = false
+  var checkValidDeref  : Boolean = false
+  var checkValidFree   : Boolean = false
+  var checkMemCleanup  : Boolean = false
+
+  /**
+   * memtrack is not directly supported by TriCera. Instead, we check for
+   * the stronger property memcleanup - safe means safe for memtrack, unsafe
+   * means inconclusive.
+   * @todo Support memtrack and remove the following field, refactoring the code
+   *       that refer to it.
+   */
+  val useMemCleanupForMemTrack = true
+
+  /**
+   * If set, will check all properties in [[memSafetyProperties]].
+   * This set should reflect the memsafety category of SV-COMP.
+   */
+  var checkMemSafety : Boolean = false
+  val memSafetyProperties = {
+    import tricera.properties._
+    Set(MemValidDeref, MemValidTrack, MemValidFree)
+  }
+
+  /**
+   * If set, will verify each property separately.
+   */
+  var splitProperties : Boolean = false
 
   var useArraysForHeap : Boolean = false
 
@@ -92,7 +126,7 @@ class TriCeraParameters extends GlobalParameters {
 
   private val greeting =
     "TriCera v" + version + ".\n(C) Copyright " +
-      "2012-2023 Zafer Esen and Philipp Ruemmer\n" +
+      "2012-2024 Zafer Esen and Philipp Ruemmer\n" +
     "Contributors: Pontus Ernstedt, Hossein Hojjat"
 
   private def parseArgs(args: List[String], shouldExecute : Boolean = true): Boolean =
@@ -119,7 +153,6 @@ class TriCeraParameters extends GlobalParameters {
     case "-inv" :: rest => inferLoopInvariants = true; parseArgs(rest)
     case "-acsl" :: rest => displayACSL = true; parseArgs(rest)
 
-    case "-memtrack" :: rest => shouldTrackMemory = true; parseArgs(rest)
     case "-mathArrays" :: rest => useArraysForHeap = true; parseArgs(rest)
 
     case "-abstract" :: rest => templateBasedInterpolation = true; parseArgs(rest)
@@ -251,77 +284,96 @@ class TriCeraParameters extends GlobalParameters {
     case symexDepthOpt :: rest if (symexDepthOpt.startsWith("-symDepth:")) =>
       symexMaxDepth = Some(symexDepthOpt.drop("-symDepth:".length).toInt)
       parseArgs(rest)
+
+    case "-reachsafety"      :: rest => checkReachSafety = true; parseArgs(rest)
+    case "-memsafety"        :: rest => checkMemSafety = true; parseArgs(rest)
+    case "-valid-memtrack"   :: rest => checkMemTrack = true; parseArgs(rest)
+    case "-valid-deref"      :: rest => checkValidDeref = true; parseArgs(rest)
+    case "-valid-free"       :: rest => checkValidFree = true; parseArgs(rest)
+    case "-valid-memcleanup" :: rest => checkMemCleanup = true; parseArgs(rest)
+    case "-splitProperties"  :: rest => splitProperties = true; parseArgs(rest)
+
     case arg :: rest if Set("-v", "--version").contains(arg) =>
       println(version); false
     case arg :: rest if Set("-h", "--help").contains(arg) =>
       println(greeting + "\n\nUsage: tri [options] file\n\n" +
-      "General options:\n" +
-      " -h, --help\t\tShow this information\n" +
-      " -v, --version\tPrint version number\n" +
-      " -arithMode:t\tInteger semantics: math (default), ilp32, lp64, llp64\n" +
-      " -mathArrays:t\tUse mathematical arrays for modeling program arrays (no implicit memory safety properties))\n" +
-      " -memtrack\tCheck that there are no memory leaks in the input program \n" +
-      " -t:time\tSet timeout (in seconds)\n" +
-      " -cex\t\tShow textual counterexamples\n" +
-      " -dotCEX\tOutput counterexample in dot format\n" +
-      " -eogCEX\tDisplay counterexample using eog on Linux and Preview on macOS\n" +
-      " -sol\t\tShow solution in Prolog format\n" +
-      " -ssol\t\tShow solution in SMT-LIB format\n" +
-      " -inv\t\tTry to infer loop invariants\n" +
-      " -acsl\t\tPrint inferred ACSL annotations\n" +
-      " -log:n            Display progress based on verbosity level n (0 <= n <= 3)\n" +
-      "                     1: Statistics only\n" +
-      "                     2: Include invariants\n" +
-      "                     3: Include counterexamples\n" +
-      "                     (When using -sym, n > 1 displays derived clauses.) \n" +
-      " -statistics       Equivalent to -log:1; displays statistics only\n" +
-      " -log              Equivalent to -log:2; displays progress and invariants\n" +
-      " -logPreds: Log only predicates containing the specified substrings,\n" +
-      "                     separated by commas. E.g., -logPreds=p1,p2 logs any\n" +
-      "                     predicate with 'p1' or 'p2' in its name\n" +
-      " -m:func\tUse function func as entry point (default: main)\n" +
-      " -cpp\t\tExecute the C preprocessor (cpp) on the input file first, this will produce filename.i\n" +
-      "\n" +
-      "Horn clauses:\n" +
-      " -p\t\tPretty-print Horn clauses\n" +
-      " -pDot\t\tPretty-print Horn clauses, output in dot format and display it\n" +
-      " -sp\t\tPretty-print the Horn clauses in SMT-LIB format\n" +
-      " -dumpClauses\tWrite the Horn clauses in SMT-LIB format to input filename.smt2\n" +
-      " -varLines\tPrint program variables in clauses together with their line numbers (e.g., x:42)\n" +
-      "\n" +
-      "Horn engine options (Eldarica):\n" +
-      " -sym            (Experimental) Use symbolic execution with the default engine (bfs)\n" +
-      " -sym:x          Use symbolic execution where x : {dfs, bfs}\n" +
-      "                      dfs: depth-first forward (does not support non-linear clauses)\n" +
-      "                      bfs: breadth-first forward\n" +
-      " -symDepth:n     Set a max depth for symbolic execution (underapproximate)\n" +
-      "                     (currently only supported with bfs)\n" +
-      " -disj\t\tUse disjunctive interpolation\n" +
-      " -stac\t\tStatic acceleration of loops\n" +
-      " -lbe\t\tDisable preprocessor (e.g., clause inlining)\n" +
-      " -arrayQuans:n\tIntroduce n quantifiers for each array argument (default: 1)\n" +
-      " -noSlicing\tDisable slicing of clauses\n" +
-      " -hints:f\tRead initial predicates and abstraction templates from a file\n" +
-      "\n" +
-      " -abstract:t\tInterp. abstraction: off, manual, term, oct,\n" +
-      "            \t                     relEqs (default), relIneqs\n" +
-      " -abstractTO:t\tTimeout (s) for abstraction search (default: 2.0)\n" +
-      " -abstractPO\tRun with and w/o interpolation abstraction in parallel\n" +
-      " -splitClauses:n\tAggressiveness when splitting disjunctions in clauses\n" +
-      "                \t                     (0 <= n <= 2, default: 1)\n" +
-      " -pHints\t\tPrint initial predicates and abstraction templates\n" +
-      "\n" +
-      "TriCera preprocessor:\n" +
-      " -printPP\tPrint the output of the TriCera preprocessor to stdout\n" +
-      " -dumpPP\tDump the output of the TriCera preprocessor to file (input file name + .tri) \n" +
-      " -logPP:n\tDisplay TriCera preprocessor warnings and errors with verbosity n (currently 0 <= n <= 2)\n" +
-      " -noPP\t\tTurn off the TriCera preprocessor (typedefs are not allowed in this mode) \n" +
-      "\n" +
-      "Debugging:\n" +
-      " -assert\t\tEnable assertions in TriCera\n" +
-      " -assertNoVerify\tEnable assertions, but do not verify solutions \n"
-//      " -pc\t\tPrint path constraint formula at return from entry function\n" (not currently correct)
-    )
+  """General options:
+    |-h, --help         Show this information
+    |-v, --version      Print version number
+    |-arithMode:t       Integer semantics: math (default), ilp32, lp64, llp64
+    |-mathArrays:t      Use mathematical arrays for modeling program arrays (ignores memsafety properties)
+    |-t:time            Set timeout (in seconds)
+    |-cex               Show textual counterexamples
+    |-dotCEX            Output counterexample in dot format
+    |-eogCEX            Display counterexample using eog on Linux and Preview on macOS
+    |-sol               Show solution in Prolog format
+    |-ssol              Show solution in SMT-LIB format
+    |-inv               Try to infer loop invariants
+    |-acsl              Print inferred ACSL annotations
+    |-log:n             Display progress based on verbosity level n (0 <= n <= 3)
+    |                     1: Statistics only
+    |                     2: Include invariants
+    |                     3: Include counterexamples
+    |                     (When using -sym, n > 1 displays derived clauses.)
+    |-statistics        Equivalent to -log:1; displays statistics only
+    |-log               Equivalent to -log:2; displays progress and invariants
+    |-logPreds:  Log only predicates containing the specified substrings,
+    |                     separated by commas. E.g., -logPreds=p1,p2 logs any
+    |                     predicate with 'p1' or 'p2' in its name
+    |-m:func            Use function func as entry point (default: main)
+    |-cpp               Execute the C preprocessor (cpp) on the input file first, this will produce filename.i
+
+    |Checked properties:
+    |-reachsafety       Enables checking of explicitly specified properties via assert statements.
+    |                   (Enabled by default unless other properties are specified.)
+    |-memsafety         Enables checking of all memory safety properties, reflecting the
+    |                   memsafety category of SV-COMP. Includes valid-deref, valid-memtrack,
+    |                   and valid-free checks.
+    |-valid-memtrack    Checks that all allocated memory is tracked.
+    |-valid-deref       Checks the validity of pointer dereferences and array accesses.
+    |-valid-free        Checks that all occurrences of 'free' are valid.
+    |-valid-memcleanup  Checks that all allocated memory is deallocated before program termination.
+    |-splitProperties   Check each property separately.
+
+    |Horn clauses:
+    |-p                 Pretty-print Horn clauses
+    |-pDot              Pretty-print Horn clauses, output in dot format and display it
+    |-sp                Pretty-print the Horn clauses in SMT-LIB format
+    |-dumpClauses       Write the Horn clauses in SMT-LIB format to input filename.smt2
+    |-varLines          Print program variables in clauses together with their line numbers (e.g., x:42)
+
+    |Horn engine options (Eldarica):
+    |-sym               (Experimental) Use symbolic execution with the default engine (bfs)
+    |-sym:x             Use symbolic execution where x : {dfs, bfs}
+    |                     dfs: depth-first forward (does not support non-linear clauses)
+    |                     bfs: breadth-first forward
+    |-symDepth:n        Set a max depth for symbolic execution (underapproximate)
+    |                     (currently only supported with bfs)
+    |-disj              Use disjunctive interpolation
+    |-stac              Static acceleration of loops
+    |-lbe               Disable preprocessor (e.g., clause inlining)
+    |-arrayQuans:n      Introduce n quantifiers for each array argument (default: 1)
+    |-noSlicing         Disable slicing of clauses
+    |-hints:f           Read initial predicates and abstraction templates from a file
+
+    |-abstract:t        Interp. abstraction: off, manual, term, oct,
+    |                     relEqs (default), relIneqs
+    |-abstractTO:t      Timeout (s) for abstraction search (default: 2.0)
+    |-abstractPO        Run with and w/o interpolation abstraction in parallel
+    |-splitClauses:n    Aggressiveness when splitting disjunctions in clauses
+    |                     (0 <= n <= 2, default: 1)
+    |-pHints            Print initial predicates and abstraction templates
+
+    |TriCera preprocessor:
+    |-printPP           Print the output of the TriCera preprocessor to stdout
+    |-dumpPP            Dump the output of the TriCera preprocessor to file (input file name + .tri)
+    |-logPP:n           Display TriCera preprocessor warnings and errors with verbosity n (currently 0 <= n <= 2)
+    |-noPP              Turn off the TriCera preprocessor (typedefs are not allowed in this mode)
+
+    |Debugging:
+    |-assert            Enable assertions in TriCera
+    |-assertNoVerify    Enable assertions, but do not verify solutions
+    |""".stripMargin)
       false
     case arg :: _ if arg.startsWith("-") =>
       showHelp
diff --git a/src/tricera/parsers/YAMLParser.scala b/src/tricera/parsers/YAMLParser.scala
new file mode 100644
index 0000000..de62f25
--- /dev/null
+++ b/src/tricera/parsers/YAMLParser.scala
@@ -0,0 +1,69 @@
+/**
+ * Copyright (c) 2024 Zafer Esen. All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * * Redistributions of source code must retain the above copyright notice, this
+ *   list of conditions and the following disclaimer.
+ *
+ * * Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ *
+ * * Neither the name of the authors nor the names of their
+ *   contributors may be used to endorse or promote products derived from
+ *   this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+
+package tricera.parsers
+
+/**
+ * A parser for SV-COMP style YAML (.yml) specification files.
+ * @note The case classes should reflect the structure of the files, do not
+ *       add any new value fields to the case classes.
+ */
+object YAMLParser {
+  case class BMOption(language : String, data_model : String)
+  case class BMPropertyFile(property_file    : String,
+                            expected_verdict : Option[Boolean] = None,
+                            subproperty      : Option[String] = None) {
+    def isReachSafety = property_file.contains("unreach-call")
+    def isMemSafety = property_file.contains("valid-memsafety")
+    def isMemCleanup = property_file.contains("valid-memcleanup")
+  }
+
+  case class BenchmarkInfo(format_version : String,
+                           input_files    : String,
+                           properties     : List[BMPropertyFile],
+                           options        : BMOption)
+
+  def extractBenchmarkInfo(yamlFileName : String): Option[BenchmarkInfo] = {
+    try {
+      import net.jcazevedo.moultingyaml._
+      object BenchmarkYamlProtocol extends DefaultYamlProtocol {
+        implicit val propFormat   = yamlFormat3(BMPropertyFile)
+        implicit val optFormat    = yamlFormat2(BMOption)
+        implicit val bmInfoFormat = yamlFormat4(BenchmarkInfo)
+      }
+      import BenchmarkYamlProtocol._
+      val src     = scala.io.Source.fromFile(yamlFileName)
+      val yamlAst = src.mkString.stripMargin.parseYaml
+      src.close
+      Some(yamlAst.convertTo[BenchmarkInfo])
+    } catch {
+      case _ : Throwable => None
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/tricera/postprocessor/ACSLLineariser.scala b/src/tricera/postprocessor/ACSLLineariser.scala
index 6789282..8f50449 100644
--- a/src/tricera/postprocessor/ACSLLineariser.scala
+++ b/src/tricera/postprocessor/ACSLLineariser.scala
@@ -47,7 +47,7 @@ object ACSLLineariser {
     for ((name, consts) <- List(("universalConstants", signature.universalConstants),
       ("existentialConstants", signature.existentialConstants),
       ("functions", signature.nullaryFunctions)))
-      if (!consts.isEmpty) {
+      if (consts.nonEmpty) {
         println("\\" + name + " {")
         for (c <- consts)
           println("int " + c.name + ";")
@@ -55,7 +55,7 @@ object ACSLLineariser {
       }
 
     // declare the required predicates
-    if (!order.orderedPredicates.isEmpty) {
+    if (order.orderedPredicates.nonEmpty) {
       println("\\predicates {")
       for (pred <- order.orderedPredicates) {
         print(pred.name)
diff --git a/src/tricera/postprocessor/ADTExploder.scala b/src/tricera/postprocessor/ADTExploder.scala
index 2f5d189..db7a9cd 100644
--- a/src/tricera/postprocessor/ADTExploder.scala
+++ b/src/tricera/postprocessor/ADTExploder.scala
@@ -35,8 +35,8 @@ import ap.theories.{ADT, TheoryRegistry}
 import ap.types.{MonoSortedIFunction, SortedConstantTerm}
 
 object ADTExploder extends SolutionProcessor {
-  def apply(expr : IExpression) : IExpression =
-    Rewriter.rewrite(expr, explodeADTs)
+  def apply(expr : IFormula) : IFormula =
+    Rewriter.rewrite(expr, explodeADTs).asInstanceOf[IFormula]
 
   case class ADTTerm(t : ITerm, adtSort : ADTProxySort)
   object adtTermExploder extends CollectingVisitor[Object, IExpression] {
diff --git a/src/tricera/postprocessor/SolutionPreprocessor.scala b/src/tricera/postprocessor/SolutionProcessor.scala
similarity index 93%
rename from src/tricera/postprocessor/SolutionPreprocessor.scala
rename to src/tricera/postprocessor/SolutionProcessor.scala
index 7052758..a7126a9 100644
--- a/src/tricera/postprocessor/SolutionPreprocessor.scala
+++ b/src/tricera/postprocessor/SolutionProcessor.scala
@@ -33,7 +33,7 @@ import ap.parser._
 import IExpression.Predicate
 
 object SolutionProcessor {
-  type Solution = Map[Predicate, IExpression]
+  type Solution = Map[Predicate, IFormula]
 }
 
 trait SolutionProcessor {
@@ -55,8 +55,8 @@ trait SolutionProcessor {
 
   /**
    * This is the function that should be implemented in new solution processors
-   * @param expr : IExpression to process
-   * @return     : processed IExpression
+   * @param expr : IFormula to process
+   * @return     : processed IFormula
    */
-  def apply(expr : IExpression) : IExpression
+  def apply(expr : IFormula) : IFormula
 }
diff --git a/src/tricera/properties/package.scala b/src/tricera/properties/package.scala
new file mode 100644
index 0000000..1158f8d
--- /dev/null
+++ b/src/tricera/properties/package.scala
@@ -0,0 +1,165 @@
+/**
+ * Copyright (c) 2024 Zafer Esen. All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * * Redistributions of source code must retain the above copyright notice, this
+ *   list of conditions and the following disclaimer.
+ *
+ * * Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ *
+ * * Neither the name of the authors nor the names of their
+ *   contributors may be used to endorse or promote products derived from
+ *   this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+
+package tricera
+
+import ap.api.SimpleAPI
+import ap.parser.IFormula
+import tricera.Util.SourceInfo
+
+/**
+ * We define the properties (mostly) as defined in SV-COMP
+ * [[https://sv-comp.sosy-lab.org/2024/rules.php]].
+ */
+package object properties {
+  sealed trait Property
+  sealed trait SubProperty extends Property
+
+  //////////////////////////////////////////////////////////////////////////////
+  // Explicit assertions
+
+  /**
+   * Unreachability of error function: `reach_error`
+   */
+  case object Reachability extends Property {
+    override def toString : String = "unreach-call"
+  }
+
+  case object UserAssertion extends Property {
+    override def toString : String = "user-assertion"
+  }
+
+  /**
+   * Function pre-/post-conditions asserted at function entry and function
+   * call sites respectively.
+   */
+  case class FunctionPrecondition(funName : String,
+                                  srcInfo : Option[SourceInfo])
+    extends Property {
+    override def toString : String = {
+      s"precondition of function $funName" +
+      (srcInfo match {
+        case Some(info) => s" asserted at ${info.line}:${info.col}."
+        case None       => ""
+      })
+    }
+  }
+
+  case class FunctionPostcondition(funName : String,
+                                   srcInfo : Option[SourceInfo])
+    extends Property {
+    override def toString : String = {
+      s"postcondition of function $funName" +
+      (srcInfo match {
+        case Some(info) => s" asserted at ${info.line}:${info.col}."
+        case None       => ""
+      })
+    }
+  }
+
+  //////////////////////////////////////////////////////////////////////////////
+  // Memory-safety properties
+
+  /**
+   * All (reachable) `free` invocations are valid, i.e.,
+   *   - no double free,
+   *   - no free on non-null, unallocated pointers,
+   *   - no free on non-heap variables.
+   */
+  case object MemValidFree extends SubProperty {
+    override def toString : String = "valid-free"
+  }
+
+  /**
+   * All (reachable) dereferences are valid, i.e.,
+   *   - no null/uninitialized pointer dereferences,
+   *   - no out-of-bounds array access,
+   *   - type safety
+   */
+  case object MemValidDeref extends SubProperty {
+    override def toString : String = "valid-deref"
+  }
+
+  /**
+   * All allocated memory is tracked, i.e., no memory leaks. In any reachable
+   * program path,
+   *   - every allocated heap memory associated with a pointer going out of
+   *   scope is freed.
+   *   - no reassigning a valid heap pointer (pointing to allocating memory),
+   *   when only that pointer holds a reference to that memory.
+   * @note Programs terminating with allocated memory does not violate this
+   *       property, but it violates [[MemValidCleanup]].
+   * @note If there are pointers going out of scope due to a `return` from main,
+   *       those will violate this property.
+   *       See [[https://gitlab.com/sosy-lab/software/cpachecker/-/issues/657]].
+   *
+   * @todo This property is currently not directly checked by TriCera,
+   *       it checks [[MemValidCleanup]] only.
+   */
+  case object MemValidTrack extends SubProperty {
+    override def toString : String = "valid-memtrack"
+  }
+
+  /**
+   * All allocated memory is deallocated before the program terminates.
+   * This property is stronger than [[MemValidTrack]].
+   * I.e., if [[MemValidCleanup]] is true, then [[MemValidTrack]] is also true.
+   *       If [[MemValidCleanup]] is false, no conclusion can be drawn for
+   *       [[MemValidTrack]].
+   */
+  case object MemValidCleanup extends Property {
+    override def toString : String = "valid-memcleanup"
+  }
+
+  //////////////////////////////////////////////////////////////////////////////
+  // Other SV-COMP properties which TriCera currently does not check for
+
+  case object NoOverflow extends Property {
+    override def toString : String = "overflow"
+  }
+
+  // For the category 'ConcurrencySafety'
+  case object NoDataRace extends Property {
+    override def toString : String = "data-race"
+  }
+
+  // For the category 'Termination'
+  case object Termination extends Property {
+    override def toString : String = "termination"
+  }
+
+  //////////////////////////////////////////////////////////////////////////////
+  // Other properties
+
+  /**
+   * In `switch` statements that we never try to jump to a case that does not
+   * exist.
+   */
+  case object SwitchCaseValidJump extends Property
+}