Log incompleteness messages to semantics and symbolic interpreter

Not used in concrete interpreter.

The incompleteness messages could be removed from semantics but this would require
ignoring the logging buffer in all equalities between states.

src/concrete/semantics.mlw

@@ -77,6 +77,9 @@ module Buffers
 
   val function split_on_default_ifs string : list string 
 
+  let constant loop_limit_message = "[INCOMPLETE] Loop limit"
+  let constant stack_limit_message = "[INCOMPLETE] Stack limit"
+
   scope Stdout
 
     use bool.Bool
@@ -106,10 +109,10 @@ module Buffers
     let function to_stdin out =
       reverse (all_lines out)
 
-    let output str out =
+    let function output str out =
       { out with line = String.concat out.line str }
 
-    let newline out =
+    let function newline out =
       { line = ""; lines = Cons out.line out.lines }
 
     (* http://pubs.opengroup.org/onlinepubs/9699919799/utilities/V3_chap02.html#tag_18_06_03 *)
@@ -653,7 +656,8 @@ module Semantics
     eval_list_expr stk (inp, ctx, sta) es (sta1, Ok args) ->
     ctx.func_env[id] = Some ins ->
     inp.config.stack_size = Finite stk ->
-    eval_instruction stk (inp, ctx, sta) (ICallFunction id es) (sta1, ctx, BIncomplete)
+    let sta1' = { sta1 with log = Stdout.(newline (output stack_limit_message sta1.log)) } in
+    eval_instruction stk (inp, ctx, sta) (ICallFunction id es) (sta1', ctx, BIncomplete)
 
   | eval_call_function: forall stk inp ctx ctx2 sta sta1 sta2 id es args ins bhv.
     eval_list_expr stk (inp, ctx, sta) es (sta1, Ok args) ->
@@ -704,7 +708,8 @@ module Semantics
   | eval_while_loop_limit: forall stk ctr b inp ctx sta ins1 ins2.
     0 <= ctr ->
     inp.config.loop_limit = Finite ctr ->
-    eval_while stk ctr b (inp, ctx, sta) ins1 ins2 (sta, ctx, BIncomplete) ctr b
+    let sta' = { sta with log = Stdout.(newline (output loop_limit_message sta.log)) } in
+    eval_while stk ctr b (inp, ctx, sta) ins1 ins2 (sta', ctx, BIncomplete) ctr b
 
   (** Condition not normal *)
   | eval_while_abort_condition: forall stk ctr b inp ctx ctx1 sta sta1 ins1 ins2 bhv1.

src/symbolic/symbolicInterpreter.mlw

@@ -686,7 +686,7 @@ module Interpreter
             if stk = get_finite inp.config.stack_size then (* Stack overflow *)
               let aux arg =
                 let sta', _ = arg in
-                (* let sta' = { sta' with log = Stdout.(newline (output "INCOMPLETE: STACK_OVERFLOW" sta'.log)) } in *)
+                let sta' = { sta' with log = Stdout.(newline (output stack_limit_message sta'.log)) } in
                 {state=sta'; context=ctx; data=()}
               in
               Rs.({empty with failure = Cn.map aux arg_res})
@@ -695,7 +695,8 @@ module Interpreter
                 eval_list_expr stk (inp, ctx, sta) le (sta1, Ok args) ->
                 ctx.func_env[id] = Some ins ->
                 inp.config.stack_size = Finite stk ->
-                Rs.mem {state=sta1; context=ctx; data=()} BIncomplete result
+                let sta1' = { sta1 with log = Stdout.(newline (output stack_limit_message sta1.log)) } in
+                Rs.mem {state=sta1'; context=ctx; data=()} BIncomplete result
               }
             else (* Execute function *)
               let res2 =
@@ -1003,7 +1004,7 @@ module Interpreter
     }
   = let loop_limit = get_finite inp.config.loop_limit in
     if ctr = loop_limit then
-      (* let sta = { sta with log = Stdout.(newline (output "INCOMPLETE: LOOP_LIMIT" sta.log)) } in *)
+      let sta = { sta with log = Stdout.(newline (output loop_limit_message sta.log)) } in
       Rs.({empty with failure=Cn.singleton {state=sta; context=ctx; data=(ctr, b)}})
     else
       let res1_normal, res1_abort =