esbmc Inconsistent CE Trace Depending on Argument Files

There are 3 C files, when specifying them in different ways to ESBMC it produces different results:

Specifying them in different order produces a different CE trace (See Sample 1+2)
Specifying only the main file shows an error completely different (See Sample 3)
Sample 2's CE trace only shows operational models and not the source code.
The trace for State 3 (in every Sample) seems suspicious, as it's missing elements when compared to other traces. May someone confirm?

I've attached the source files I've used for this bug (I was working on ESBMC-AI), FYI I used ChatGPT to generate them: timer.zip

I need someone to confirm if all 4 points are intended behaviour or if it's buggy. I am trying to write a parser for the CE trace, so I need to know what is intended, please!

Config File:

interval-analysis = true
goto-unwind = true
unlimited-goto-unwind = true
k-induction = true
state-hashing = true
add-symex-value-sets = true
k-step = 2
floatbv = true
unlimited-k-steps = false
max-k-step = 100
memory-leak-check = true
context-bound = 2
color = true
stack-trace = true

CE 1st Sample

esbmc /tmp/esbmc-aimcgr2xcdtimer/src/main.c /tmp/esbmc-aimcgr2xcdtimer/src/clock.c /tmp/esbmc-aimcgr2xcdtimer/src/timer.c

ESBMC version 7.8.1 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
[PROGRESS] Parsing /tmp/esbmc-aimcgr2xcdtimer/src/main.c
[PROGRESS] Parsing /tmp/esbmc-aimcgr2xcdtimer/src/clock.c
[PROGRESS] Parsing /tmp/esbmc-aimcgr2xcdtimer/src/timer.c
[PROGRESS] Converting
[PROGRESS] Generating GOTO Program
GOTO program creation time: 0.472s
Interval Analysis time: 0.014s
GOTO program processing time: 0.023s
[PROGRESS] Checking base case, k = 1
[PROGRESS] Starting Bounded Model Checking
Not unwinding loop 4 iteration 1   file /home/runner/work/esbmc/esbmc/src/c2goto/library/stdlib.c line 197 column 1 function atoi
Not unwinding loop 5 iteration 1   file /home/runner/work/esbmc/esbmc/src/c2goto/library/stdlib.c line 197 column 1 function atoi
Not unwinding loop 4 iteration 1   file /home/runner/work/esbmc/esbmc/src/c2goto/library/stdlib.c line 197 column 1 function atoi
Not unwinding loop 5 iteration 1   file /home/runner/work/esbmc/esbmc/src/c2goto/library/stdlib.c line 197 column 1 function atoi
[WARNING] no body for function localtime
[WARNING] no body for function strftime
[WARNING] no body for function sleep
Not unwinding loop 12 iteration 1   file /tmp/esbmc-aimcgr2xcdtimer/src/timer.c line 14 column 3 function timer_tick
Symex completed in: 0.030s (178 assignments)
Slicing time: 0.002s (removed 67 assignments)
Generated 47 VCC(s), 41 remaining after simplification (111 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.012s
[PROGRESS] Solving with solver Boolector 3.2.3
Runtime decision procedure: 0.162s
[PROGRESS] Building error trace

[Counterexample]


State 3  thread 0
----------------------------------------------------
  argv[3] = 0

State 17 file /tmp/esbmc-aimcgr2xcdtimer/src/main.c line 14 column 3 function main thread 0
----------------------------------------------------
  seconds = 0 (00000000 00000000 00000000 00000000)

State 31 file /tmp/esbmc-aimcgr2xcdtimer/src/main.c line 17 column 3 function main thread 0
----------------------------------------------------
  clock = ( struct __anon_typedef_Clock_at_/tmp/esbmc-aimcgr2xcdtimer/src/clock_h__7_9 *)0

State 33 file /tmp/esbmc-aimcgr2xcdtimer/src/clock.c line 6 column 52 function clock_init thread 0
----------------------------------------------------
Violated property:
  file /tmp/esbmc-aimcgr2xcdtimer/src/clock.c line 6 column 52 function clock_init
  dereference failure: NULL pointer


VERIFICATION FAILED

Bug found (k = 1)

CE 2nd Sample

esbmc /tmp/esbmc-aimcgr2xcdtimer/src/timer.c /tmp/esbmc-aimcgr2xcdtimer/src/clock.c /tmp/esbmc-aimcgr2xcdtimer/src/main.c

ESBMC version 7.8.1 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
[PROGRESS] Parsing /tmp/esbmc-aimcgr2xcdtimer/src/timer.c
[PROGRESS] Parsing /tmp/esbmc-aimcgr2xcdtimer/src/clock.c
[PROGRESS] Parsing /tmp/esbmc-aimcgr2xcdtimer/src/main.c
[PROGRESS] Converting
[PROGRESS] Generating GOTO Program
GOTO program creation time: 0.473s
Interval Analysis time: 0.015s
GOTO program processing time: 0.024s
[PROGRESS] Checking base case, k = 1
[PROGRESS] Starting Bounded Model Checking
Not unwinding loop 4 iteration 1   file /home/runner/work/esbmc/esbmc/src/c2goto/library/stdlib.c line 197 column 1 function atoi
Not unwinding loop 5 iteration 1   file /home/runner/work/esbmc/esbmc/src/c2goto/library/stdlib.c line 197 column 1 function atoi
Not unwinding loop 4 iteration 1   file /home/runner/work/esbmc/esbmc/src/c2goto/library/stdlib.c line 197 column 1 function atoi
Not unwinding loop 5 iteration 1   file /home/runner/work/esbmc/esbmc/src/c2goto/library/stdlib.c line 197 column 1 function atoi
[WARNING] no body for function localtime
[WARNING] no body for function strftime
[WARNING] no body for function sleep
Not unwinding loop 13 iteration 1   file /tmp/esbmc-aimcgr2xcdtimer/src/timer.c line 14 column 3 function timer_tick
Symex completed in: 0.039s (194 assignments)
Slicing time: 0.003s (removed 79 assignments)
Generated 45 VCC(s), 43 remaining after simplification (115 assignments)
No solver specified; defaulting to Boolector
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.012s
[PROGRESS] Solving with solver Boolector 3.2.3
Runtime decision procedure: 0.171s
[PROGRESS] Building error trace

[Counterexample]


State 3  thread 0
----------------------------------------------------
  argv[3] = 0

State 5 file /home/runner/work/esbmc/esbmc/src/c2goto/library/stdlib.c line 197 column 1 function atoi thread 0
----------------------------------------------------
Violated property:
  file /home/runner/work/esbmc/esbmc/src/c2goto/library/stdlib.c line 197 column 1 function atoi
  dereference failure: NULL pointer


VERIFICATION FAILED

Bug found (k = 1)

Jan 16 '25 16:01 Yiannis128

I have just gone over it with @rafaelsamenezes and here is what I have found:

ARGV is reported in the CE

argc+argv: ESBMC does not detect argv elements are not NULL as long as each element is specified by argc

Issue: https://github.com/esbmc/esbmc/issues/170

Inconsistent CE

The inconsistent CE is a bug is caused by referencing the files in different order. The symex of the program with different order results in different unimplemented functions.

Example: [WARNING] no body for function strftime operational models
Missing operational models for time functions

Steps to Fix

Look at the goto program of each invokation
If goto program is different, check if not equivalent
If not then there is a bug in the front end
If they're equivalent, check the VCC are the same

Inconsistent VCCs

Another symptom of that is that the number of VCCs is different, they should all be the same regardless if there's missing operational models. This is a bug.

Feb 06 '25 14:02 Yiannis128

Advice for inconsistent CE: use --compact-trace as it doesn't show trace from other libraries

Feb 27 '25 09:02 Yiannis128