[alias] functions still WIP

src/plugins/alias/analysis.ml

@@ -234,7 +234,7 @@ let doFunction (kf:kernel_function) =
         let final_state : Abstract_state.t option =
           try Stmt_table.find return_stmt
           with
-            Not_found -> failwith "Houston, we have a problem"
+            Not_found -> Options.abort "Houston, we have a problem: %a has no return statement" Kernel_function.pretty kf
         in
         let summary: Abstract_state.summary =
           Abstract_state.make_summary final_state kf
@@ -244,8 +244,8 @@ let doFunction (kf:kernel_function) =
   else
     begin
       (* summary by default *)
-      Options.warning "Function %a has no definition (summary empty)"
-        Kernel_function.pretty kf;
+      (* Options.warning "Function %a has no definition (summary empty)"
+       *   Kernel_function.pretty kf; *)
       let summary: Abstract_state.summary =
         Abstract_state.make_summary (Some Abstract_state.initial_value) kf
       in

src/plugins/alias/tests/basic/oracle/assignment1.res.oracle

 [kernel] Parsing assignment1.c (with preprocessing)
 [alias] Parsing done
 [alias] Functions done
-After statement a = b; :
+Before statement a = b; :
  <list of may-alias>
-{ a; b } are aliased
 <end of list>
 
-After statement b = c; :
+Before statement b = c; :
  <list of may-alias>
-{ a; b; c } are aliased
+{ a; b } are aliased
 <end of list>
 
-After statement *a = 4; :
+Before statement *a = 4; :
  <list of may-alias>
 { a; b; c } are aliased
 <end of list>
 
-After statement *c = e; :
+Before statement *c = e; :
  <list of may-alias>
 { a; b; c } are aliased
 <end of list>
 
-After statement a = d; :
+Before statement a = d; :
  <list of may-alias>
-{ a; b; c; d } are aliased
+{ a; b; c } are aliased
 <end of list>
 
-After statement __retres = 0; :
+Before statement __retres = 0; :
  <list of may-alias>
 { a; b; c; d } are aliased
 <end of list>
 
-After statement return __retres; :
+Before statement return __retres; :
  <list of may-alias>
 { a; b; c; d } are aliased
 <end of list>

src/plugins/alias/tests/basic/oracle/assignment2.res.oracle

 [kernel] Parsing assignment2.c (with preprocessing)
 [alias] Parsing done
 [alias] Functions done
-After statement *a = b; :
+Before statement *a = b; :
  <list of may-alias>
 <end of list>
 
-After statement *c = d; :
+Before statement *c = d; :
  <list of may-alias>
 <end of list>
 
-After statement a = c; :
+Before statement a = c; :
  <list of may-alias>
-{ a; c } are aliased
-{ b; d } are aliased
 <end of list>
 
-After statement __retres = 0; :
+Before statement __retres = 0; :
  <list of may-alias>
 { a; c } are aliased
 { b; d } are aliased
 <end of list>
 
-After statement return __retres; :
+Before statement return __retres; :
  <list of may-alias>
 { a; c } are aliased
 { b; d } are aliased

src/plugins/alias/tests/basic/oracle/assignment3.res.oracle

 [kernel] Parsing assignment3.c (with preprocessing)
 [alias] Parsing done
 [alias] Functions done
-After statement a = & b; :
+Before statement a = & b; :
  <list of may-alias>
 <end of list>
 
-After statement *c = b; :
+Before statement *c = b; :
  <list of may-alias>
 <end of list>
 
-After statement __retres = 0; :
+Before statement __retres = 0; :
  <list of may-alias>
 <end of list>
 
-After statement return __retres; :
+Before statement return __retres; :
  <list of may-alias>
 <end of list>
 

src/plugins/alias/tests/basic/oracle/cast1.res.oracle

 [kernel] Parsing cast1.c (with preprocessing)
 [alias] Parsing done
 [alias] Functions done
-After statement a = (int *)c; :
+Before statement a = (int *)c; :
  <list of may-alias>
-{ a; c } are aliased
 <end of list>
 
-After statement d = (float *)b; :
+Before statement d = (float *)b; :
  <list of may-alias>
 { a; c } are aliased
-{ b; d } are aliased
 <end of list>
 
-After statement __retres = 0; :
+Before statement __retres = 0; :
  <list of may-alias>
 { a; c } are aliased
 { b; d } are aliased
 <end of list>
 
-After statement return __retres; :
+Before statement return __retres; :
  <list of may-alias>
 { a; c } are aliased
 { b; d } are aliased

src/plugins/alias/tests/basic/oracle/conditional1.res.oracle

 [kernel] Parsing conditional1.c (with preprocessing)
 [alias] Parsing done
 [alias] Functions done
-After statement if (a) a = b; else a = c; :
+Before statement if (a) a = b; else a = c; :
  <list of may-alias>
 <end of list>
 
-After statement a = b; :
+Before statement a = b; :
  <list of may-alias>
-{ a; b } are aliased
 <end of list>
 
-After statement a = c; :
+Before statement a = c; :
  <list of may-alias>
-{ a; c } are aliased
 <end of list>
 
-After statement *a = 4; :
+Before statement *a = 4; :
  <list of may-alias>
 { a; b } are aliased
 <end of list>
 
-After statement __retres = 0; :
+Before statement __retres = 0; :
  <list of may-alias>
 { a; b } are aliased
 <end of list>
 
-After statement return __retres; :
+Before statement return __retres; :
  <list of may-alias>
 { a; b } are aliased
 <end of list>

src/plugins/alias/tests/basic/oracle/function1.res.oracle

 [kernel] Parsing function1.c (with preprocessing)
 [alias] Parsing done
-[alias] Skiping swap(a,b); (summary not found)
-[alias] Skiping swap(a,b); (summary not found)
-[alias] Skiping swap(c,d); (summary not found)
-[alias] Skiping swap(c,d); (summary not found)
 [alias] Functions done
-After statement z = x; :
+Before statement z = x; :
  <list of may-alias>
-{ x; z } are aliased
 <end of list>
 
-After statement x = y; :
+Before statement z = x; :
  <list of may-alias>
-{ x; y; z } are aliased
 <end of list>
 
-After statement y = z; :
+Before statement x = y; :
+ <list of may-alias>
+{ x; z } are aliased
+<end of list>
+
+Before statement y = z; :
  <list of may-alias>
 { x; y; z } are aliased
 <end of list>
 
-After statement swap(a,b); :
+Before statement swap(a,b); :
  <list of may-alias>
 <end of list>
 
-After statement swap(c,d); :
+Before statement swap(c,d); :
  <list of may-alias>
+{ a; b } are aliased
 <end of list>
 
-After statement __retres = 0; :
+Before statement __retres = 0; :
  <list of may-alias>
+{ a; b } are aliased
+{ c; d } are aliased
 <end of list>
 
-After statement return; :
+Before statement return; :
  <list of may-alias>
 { x; y; z } are aliased
 <end of list>
 
-After statement return __retres; :
+Before statement return __retres; :
  <list of may-alias>
+{ a; b } are aliased
+{ c; d } are aliased
 <end of list>
 
 [alias] Analysis complete

src/plugins/alias/tests/basic/oracle/while_for1.res.oracle

@@ -4,67 +4,67 @@
 [alias] Skipping assignment odata[idx] = 0.5 * idata[idx] (not implemented)
 [alias] Skipping assignment odata[idx] = 0.5 * idata[idx] (not implemented)
 [alias] Functions done
-After statement while (1) {
-                  idx = 0;
-                  while (idx < 10) {
-                    odata[idx] = 0.5 * idata[idx];
-                    idx ++;
-                  }
-                } :
+Before statement while (1) {
+                   idx = 0;
+                   while (idx < 10) {
+                     odata[idx] = 0.5 * idata[idx];
+                     idx ++;
+                   }
+                 } :
  <list of may-alias>
 <end of list>
 
-After statement idx = 0;
-                while (idx < 10) {
-                  odata[idx] = 0.5 * idata[idx];
-                  idx ++;
-                } :
+Before statement idx = 0;
+                 while (idx < 10) {
+                   odata[idx] = 0.5 * idata[idx];
+                   idx ++;
+                 } :
  <list of may-alias>
 <end of list>
 
-After statement idx = 0; :
+Before statement idx = 0; :
  <list of may-alias>
 <end of list>
 
-After statement idx = 0; :
+Before statement idx = 0; :
  <list of may-alias>
 <end of list>
 
-After statement while (idx < 10) {
-                  odata[idx] = 0.5 * idata[idx];
-                  idx ++;
-                } :
+Before statement while (idx < 10) {
+                   odata[idx] = 0.5 * idata[idx];
+                   idx ++;
+                 } :
  <list of may-alias>
 <end of list>
 
-After statement while (idx < 10) {
-                  odata[idx] = 0.5 * idata[idx];
-                  idx ++;
-                } :
+Before statement while (idx < 10) {
+                   odata[idx] = 0.5 * idata[idx];
+                   idx ++;
+                 } :
  <list of may-alias>
 <end of list>
 
-After statement if (! (idx < 10)) break; :
+Before statement if (! (idx < 10)) break; :
  <list of may-alias>
 <end of list>
 
-After statement break; :
+Before statement break; :
  <list of may-alias>
 <end of list>
 
-After statement odata[idx] = 0.5 * idata[idx]; :
+Before statement odata[idx] = 0.5 * idata[idx]; :
  <list of may-alias>
 <end of list>
 
-After statement odata[idx] = 0.5 * idata[idx]; :
+Before statement odata[idx] = 0.5 * idata[idx]; :
  <list of may-alias>
 <end of list>
 
-After statement odata[idx] = 0.5 * idata[idx]; :
+Before statement odata[idx] = 0.5 * idata[idx]; :
  <list of may-alias>
 <end of list>
 
-After statement idx ++; :
+Before statement idx ++; :
  <list of may-alias>
 <end of list>