Replace violation cram test

Author: karoliineh

tests/regression/witness/violation.t/callfpointer.c

@@ -0,0 +1,34 @@
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "nec11.c", 3, "reach_error"); }
+
+void __VERIFIER_assert(int cond) {
+  if (!(cond)) {
+    ERROR: {reach_error();abort();}
+  }
+  return;
+}
+
+_Bool __VERIFIER_nondet_bool();
+
+int main(){
+   int a[5];
+   int len=0;
+   _Bool c=__VERIFIER_nondet_bool();
+   int i;
+
+
+   while(c){
+     
+      if (len==4)
+         len =0;
+      
+      a[len]=0;
+
+      len++;
+   }
+   __VERIFIER_assert(len==5);
+   return 1;
+
+   
+}

tests/regression/witness/violation.t/nec11.c

@@ -1,82 +1,22 @@
-  $ goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )"} callfpointer.c --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty --enable ana.wp  --set witness.yaml.entry-types[+] violation_sequence --enable witness.yaml.sv-comp-true-only --enable witness.invariant.other 
+  $ goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )"} nec11.c --enable exp.arg.enabled --enable ana.wp --set witness.yaml.entry-types[+] violation_sequence --enable witness.yaml.sv-comp-true-only --enable witness.invariant.other 
   [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
-  [Warning][Deadcode] Function 'main' does not return
-  [Warning][Deadcode] Function 'f' has dead code:
-    on line 8 (callfpointer.c:8-8)
-  [Warning][Deadcode] Function 'h' has dead code:
-    on line 16 (callfpointer.c:16-16)
-  [Warning][Deadcode] Function 'main' has dead code:
-    on line 20 (callfpointer.c:20-20)
-  [Warning][Deadcode] Logical lines of code (LLoC) summary:
-    live: 8
-    dead: 3
-    total lines: 11
-  [Warning][Deadcode][CWE-571] condition 'i == 1' is always true (callfpointer.c:11:5-11:9)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow (nec11.c:28:7-28:12)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 16
+    dead: 0
+    total lines: 16
   SV-COMP result: unknown
 
-  $ graph-easy --as=boxart arg.dot
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ Entry main
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ InlineEntry '(& h)'
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ Entry f
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ InlineEntry '(1)'
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ Entry h
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ Test (i == 1,true)
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ InlineEntry '()'
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-    │
-    │ Entry reach_error
-    ▼
-  ┌──────────────────────┐
-  │          _           │
-  └──────────────────────┘
-
   $ yamlWitnessStrip < witness.yml
   - entry_type: violation_sequence
     content:
     - segment:
       - waypoint:
           type: assumption
           location:
-            file_name: callfpointer.c
-            line: 18
-            column: 2
+            file_name: nec11.c
+            line: 16
+            column: 4
             function: main
           action: follow
           constraint:
@@ -86,10 +26,10 @@
       - waypoint:
           type: assumption
           location:
-            file_name: callfpointer.c
-            line: 7
-            column: 2
-            function: f
+            file_name: nec11.c
+            line: 17
+            column: 4
+            function: main
           action: follow
           constraint:
             value: "1"
@@ -98,10 +38,34 @@
       - waypoint:
           type: branching
           location:
-            file_name: callfpointer.c
-            line: 11
-            column: 2
-            function: h
+            file_name: nec11.c
+            line: 21
+            column: 4
+            function: main
+          action: follow
+          constraint:
+            value: "false"
+            format: c_expression
+    - segment:
+      - waypoint:
+          type: assumption
+          location:
+            file_name: nec11.c
+            line: 30
+            column: 4
+            function: main
+          action: follow
+          constraint:
+            value: "1"
+            format: c_expression
+    - segment:
+      - waypoint:
+          type: branching
+          location:
+            file_name: nec11.c
+            line: 6
+            column: 3
+            function: __VERIFIER_assert
           action: follow
           constraint:
             value: "true"
@@ -110,8 +74,8 @@
       - waypoint:
           type: target
           location:
-            file_name: callfpointer.c
-            line: 12
-            column: 11
-            function: h
+            file_name: nec11.c
+            line: 7
+            column: 13
+            function: __VERIFIER_assert
           action: follow