diff --git a/tests/spec/const_fold_term.i b/tests/spec/const_fold_term.i index c2f4bb8b69ca445cb6122eef5c8b69feda62c269..dcabf3bd580cb2b7f73e8026240336341dd6388b 100644 --- a/tests/spec/const_fold_term.i +++ b/tests/spec/const_fold_term.i @@ -14,9 +14,9 @@ void binop(int a) { //@ assert 84 - 42 == 42; //@ assert 6 * 7 == 42; //@ assert 21 << 1 == 42; - //@ assert 672 >> 4 == 42; + //@ assert 672 >> sizeof(int) == 42; //@ assert (58 & 47) == 42; - //@ assert (34 | 8) == 42; + //@ assert (34 | sizeof("frama-c")) == 42; //@ assert (63 ^ 21) == 42; - //@ assert 168 / 4 == 42; + //@ assert 168 / sizeof(a) == 42; } diff --git a/tests/spec/const_fold_term.ml b/tests/spec/const_fold_term.ml index 4daf0015f496833e27acbdc4770eabd231c972b2..fe52ad8ac04840bd99a60ada938da688e40078e5 100644 --- a/tests/spec/const_fold_term.ml +++ b/tests/spec/const_fold_term.ml @@ -13,7 +13,7 @@ class visitTerm prj = object(_) method! vterm t = fold t; - Cil.DoChildren + Cil.JustCopy end @@ -22,15 +22,27 @@ let test_terms () = let loc = Cil_datatype.Location.unknown in let e1 = lognot ((of_int 21) + (of_int 21)) in let e2 = lognot ((of_int 21) - (of_int 21)) in + let e3 = lt zero (logand (of_int 42) (of_int 21)) in + let e4 = gt one (logor zero (of_int 21)) in + let e5 = ne zero (le zero (logand (of_int 42) (of_int 21))) in + let e6 = eq one (ge one (logor one zero)) in let t1 = cil_term ~loc e1 in let t2 = cil_term ~loc e2 in - Format.printf "Custom terms : @."; + let t3 = cil_term ~loc e3 in + let t4 = cil_term ~loc e4 in + let t5 = cil_term ~loc e5 in + let t6 = cil_term ~loc e6 in + Format.printf "Custom terms :@."; fold t1; - fold t2 + fold t2; + fold t3; + fold t4; + fold t5; + fold t6 let startup () = test_terms (); - Format.printf "File terms : @."; + Format.printf "File terms :@."; let prj = File.create_project_from_visitor "test_const_fold" (fun prj -> new visitTerm prj) in diff --git a/tests/spec/oracle/const_fold_term.res.oracle b/tests/spec/oracle/const_fold_term.res.oracle index 42efc6ac9ea7d2491ce118eab4c784ea56bbd7ff..61d1b054b90db6295840d234120d6fe05db78d81 100644 --- a/tests/spec/oracle/const_fold_term.res.oracle +++ b/tests/spec/oracle/const_fold_term.res.oracle @@ -1,19 +1,21 @@ [kernel] Parsing const_fold_term.i (no preprocessing) -Custom terms : +Custom terms : !(21 + 21) folds to 0 !(21 - 21) folds to 1 -File terms : + 0 < (42 ∧ 21) folds to 1 + 1 > (0 ∨ 21) folds to 0 + 0 ≢ (0 ≤ (42 ∧ 21)) folds to 1 + 1 ≡ (1 ≥ (1 ∨ 0)) folds to 1 +File terms : -(21 + 21) folds to -42 - 21 + 21 folds to 42 ~21 folds to -22 -a folds to -a - (21 + 21) + a folds to (21 + 21) + a - 21 + 21 folds to 42 + (21 + 21) + a folds to 42 + a 84 - 42 folds to 42 6 * 7 folds to 42 21 << 1 folds to 42 - 672 >> 4 folds to 42 + 672 >> sizeof(int) folds to 42 58 & 47 folds to 42 - 34 | 8 folds to 42 + 34 | sizeof("frama-c") folds to 42 63 ^ 21 folds to 42 - 168 / 4 folds to 168 / 4 + 168 / sizeof(a) folds to 168 / 4