Skip to content
Snippets Groups Projects
Commit f44defcb authored by Pierre Nigron's avatar Pierre Nigron Committed by Virgile Prevosto
Browse files

[test] Tests + Oracles

parent dff604ea
No related branches found
No related tags found
No related merge requests found
...@@ -12,7 +12,7 @@ ...@@ -12,7 +12,7 @@
[rte] addsub_typedef.c:13: Warning: [rte] addsub_typedef.c:13: Warning:
guaranteed RTE: guaranteed RTE:
assert assert
signed_overflow: -2147483648 ≤ (tint)(-((int)((int)(-0x7fffffff) - 1))) - 1; signed_overflow: -2147483648 ≤ (int)(-((int)((int)(-0x7fffffff) - 1))) - 1;
/* Generated by Frama-C */ /* Generated by Frama-C */
typedef int tint; typedef int tint;
int main(void) int main(void)
...@@ -30,7 +30,7 @@ int main(void) ...@@ -30,7 +30,7 @@ int main(void)
/*@ assert rte: signed_overflow: -2147483647 ≤ (int)(-0x7fffffff) - 1; */ /*@ assert rte: signed_overflow: -2147483647 ≤ (int)(-0x7fffffff) - 1; */
/*@ assert /*@ assert
rte: signed_overflow: rte: signed_overflow:
-2147483648 ≤ (tint)(-((int)((int)(-0x7fffffff) - 1))) - 1; -2147483648 ≤ (int)(-((int)((int)(-0x7fffffff) - 1))) - 1;
*/ */
z = - (-0x7fffffff - 1) - 1; z = - (-0x7fffffff - 1) - 1;
z = 0x7fffffff + 0; z = 0x7fffffff + 0;
...@@ -38,8 +38,7 @@ int main(void) ...@@ -38,8 +38,7 @@ int main(void)
/*@ assert rte: signed_overflow: -2147483648 ≤ x + y; */ /*@ assert rte: signed_overflow: -2147483648 ≤ x + y; */
/*@ assert rte: signed_overflow: x + y ≤ 2147483647; */ /*@ assert rte: signed_overflow: x + y ≤ 2147483647; */
z = x + y; z = x + y;
/*@ assert rte: signed_overflow: -2147483648 ≤ (tint)(-0x7ffffffc) - y; /*@ assert rte: signed_overflow: -2147483648 ≤ (int)(-0x7ffffffc) - y; */
*/
z = -0x7ffffffc - y; z = -0x7ffffffc - y;
/*@ assert rte: signed_overflow: -2147483647 ≤ x; */ /*@ assert rte: signed_overflow: -2147483647 ≤ x; */
/*@ assert rte: signed_overflow: -2147483648 ≤ (tint)(-x) - 0x7ffffffc; /*@ assert rte: signed_overflow: -2147483648 ≤ (tint)(-x) - 0x7ffffffc;
......
open Cil_types open Cil_types
let warn_cast = let warn_cast =
let typeForInsertedCast = !Cabs2cil.typeForInsertedCast in let typeForInsertedCast = !Cil.typeForInsertedCast in
fun e t1 t2 -> fun e t1 t2 ->
Kernel.feedback ~source:(fst e.eloc) "Inserted implicit cast from %a to %a" Kernel.feedback ~source:(fst e.eloc) "Inserted implicit cast from %a to %a"
Printer.pp_typ t1 Printer.pp_typ t2; Printer.pp_typ t1 Printer.pp_typ t2;
typeForInsertedCast e t1 t2 typeForInsertedCast e t1 t2
let () = Cabs2cil.typeForInsertedCast := warn_cast let () = Cil.typeForInsertedCast := warn_cast
let run () = let run () =
let f = Ast.get () in let f = Ast.get () in
......
...@@ -11,4 +11,4 @@ let print_warning e ot nt = ...@@ -11,4 +11,4 @@ let print_warning e ot nt =
nt nt
;; ;;
Cabs2cil.typeForInsertedCast := print_warning Cil.typeForInsertedCast := print_warning
[kernel] Parsing array_cast_bts1099.i (no preprocessing) [kernel] Parsing array_cast_bts1099.i (no preprocessing)
[kernel] array_cast_bts1099.i:12: User Error: [kernel] array_cast_bts1099.i:12: User Error:
explicit cast: cast over a non-scalar type t Cast over a non-scalar type t
10 int tab1[4]; 10 int tab1[4];
11 u* p = &tab1; 11 u* p = &tab1;
12 t* p2 = (t) p; 12 t* p2 = (t) p;
......
[kernel] Parsing wrong-assignment.i (no preprocessing) [kernel] Parsing wrong-assignment.i (no preprocessing)
[kernel] wrong-assignment.i:13: User Error: [kernel] wrong-assignment.i:13: User Error:
implicit cast: ebool -> _Bool cast from ebool to _Bool
11 void d() { 11 void d() {
12 // this assignment should be rejected 12 // this assignment should be rejected
13 c.a = b; 13 c.a = b;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment