Fix basic functionality of topdown_term

Author: sim642

src/solver/topDown_term.ml

@@ -24,8 +24,8 @@ module WP =
       let stable = HM.create  10 in
       let infl   = HM.create  10 in (* y -> xs *)
       let called = HM.create  10 in
-      let rho    = HM.create  10 in
-      let rho'   = HM.create  10 in
+      let rho    = HM.create  10 in (* rho for right-hand side values *)
+      let rho'   = HM.create  10 in (* rho for start and side effect values *)
       let wpoint = HM.create  10 in
 
       let add_infl y x =
@@ -101,7 +101,7 @@ module WP =
       let set_start (x,d) =
         if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d;
         init x;
-        HM.replace rho x d;
+        HM.replace rho' x d;
         solve x Widen
       in
 

tests/regression/00-sanity/01-assert.t

@@ -65,51 +65,16 @@ Test topdown solvers:
     total lines: 9
 
   $ goblint --enable warn.deterministic --set solver topdown_term 01-assert.c
-  [Error] Fixpoint not reached at L:entry state of main (299) on 01-assert.c:4:1-15:1
-   Solver computed:
-   bot
-   Right-Hand-Side:
-   HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(),
-                                                                                                                   mallocWrapper:(wrapper call:Unknown node, unique calls:{}),
-                                                                                                                   base:({
-                                                                                                                           }, {}, {}, {}),
-                                                                                                                   threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
-                                                                                                                   threadflag:Singlethreaded,
-                                                                                                                   threadreturn:true,
-                                                                                                                   escape:{},
-                                                                                                                   mutexEvents:(),
-                                                                                                                   access:(),
-                                                                                                                   mutex:(lockset:{}, multiplicity:{}),
-                                                                                                                   race:(),
-                                                                                                                   mhp:(),
-                                                                                                                   assert:(),
-                                                                                                                   pthreadMutexType:()], map:{})}
-   Difference: HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):PathSensitive (ProjectiveSet (MCP.D * map)):{(MCP.D:[expRelation:(),
-                                                                                                                               mallocWrapper:(wrapper call:Unknown node, unique calls:{}),
-                                                                                                                               base:({
-                                                                                                                                       }, {}, {}, {}),
-                                                                                                                               threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
-                                                                                                                               threadflag:Singlethreaded,
-                                                                                                                               threadreturn:true,
-                                                                                                                               escape:{},
-                                                                                                                               mutexEvents:(),
-                                                                                                                               access:(),
-                                                                                                                               mutex:(lockset:{}, multiplicity:{}),
-                                                                                                                               race:(),
-                                                                                                                               mhp:(),
-                                                                                                                               assert:(),
-                                                                                                                               pthreadMutexType:()], map:{})} instead of bot
-  
+  [Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
+  [Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
+  [Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
   [Warning][Deadcode] Function 'main' does not return
   [Warning][Deadcode] Function 'main' has dead code:
-    on lines 4..7 (01-assert.c:4-7)
-    on lines 10..14 (01-assert.c:10-14)
+    on lines 13..14 (01-assert.c:13-14)
   [Warning][Deadcode] Logical lines of code (LLoC) summary:
-    live: 0
-    dead: 9
+    live: 7
+    dead: 2
     total lines: 9
-  [Error][Unsound] Fixpoint not reached
-  [3]
 
   $ goblint --enable warn.deterministic --set solver topdown_space_cache_term 01-assert.c
   [Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)