search

TrustInSoft / tis-interpreter

An interpreter for finding subtle bugs in programs written in standard C
565 stars 28 forks source link

Unexpected error: assignment of structs with flexible array members #114

Closed ch3root closed 8 years ago

ch3root commented 8 years ago

Source code:

int main()
{
  struct { char c; char a[]; } x, y;
  y = x;
}

tis-interpreter (31be1ffdb350ea940095be4757d0d5779c38f10b) output:

[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[kernel] Current source was: test.c:4
         The full backtrace is:
         Raised at file "src/plugins/value/legacy/eval_stmt.ml", line 65, characters 27-39
         Called from file "list.ml", line 84, characters 24-34
         Called from file "src/plugins/value/legacy/eval_stmt.ml", line 171, characters 6-162
         Called from file "src/plugins/value/legacy/eval_stmt.ml", line 330, characters 30-73
         Called from file "src/plugins/value/legacy/eval_stmt.ml", line 356, characters 33-56
         Called from file "src/plugins/value/legacy/eval_stmt.ml", line 369, characters 10-30
         Called from file "src/plugins/value/legacy/eval_stmt.ml", line 394, characters 8-97
         Called from file "src/plugins/value/legacy/eval_stmt.ml", line 400, characters 6-70
         Called from file "src/plugins/value/legacy/eval_slevel.ml", line 562, characters 30-38
         Called from file "list.ml", line 84, characters 24-34
         Called from file "src/plugins/value/legacy/eval_slevel.ml", line 559, characters 14-326
         Called from file "src/plugins/value/legacy/eval_slevel.ml", line 572, characters 14-175
         Called from file "src/libraries/utils/statistics.ml", line 333, characters 21-29
         Re-raised at file "src/libraries/utils/statistics.ml", line 338, characters 14-15
         Called from file "src/kernel_services/analysis/dataflow2.ml", line 362, characters 28-46
         Called from file "src/kernel_services/analysis/dataflow2.ml", line 512, characters 14-39
         Called from file "src/plugins/value/legacy/eval_funs.ml", line 58, characters 8-36
         Called from file "src/plugins/value/legacy/eval_funs.ml", line 147, characters 8-61
         Called from file "src/plugins/value/legacy/eval_funs.ml", line 307, characters 14-117
         Re-raised at file "src/plugins/value/legacy/eval_funs.ml", line 311, characters 14-15
         Called from file "src/libraries/utils/statistics.ml", line 333, characters 21-29
         Re-raised at file "src/libraries/utils/statistics.ml", line 338, characters 14-15
         Called from file "src/plugins/value/legacy/eval_funs.ml", line 690, characters 11-40
         Re-raised at file "src/plugins/value/legacy/eval_funs.ml", line 718, characters 47-50
         Called from file "src/libraries/project/state_builder.ml", line 978, characters 9-13
         Re-raised at file "src/libraries/project/state_builder.ml", line 986, characters 15-18
         Called from file "src/plugins/value/register.ml", line 108, characters 4-24
         Called from file "queue.ml", line 134, characters 6-20
         Called from file "src/kernel_internals/runtime/boot.ml", line 39, characters 4-20
         Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 783, characters 2-9
         Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 813, characters 18-64
         Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 224, characters 4-8

         Unexpected error (File "src/plugins/value/legacy/eval_stmt.ml", line 65, characters 27-33: Assertion failed).
         Please report at https://github.com/TrustInSoft/tis-interpreter/issues
pascal-cuoq commented 8 years ago

I am investigating other problems in relation to flexible array members (yes, beyond the wave that you already reported), it will be nice when everything is working more correctly.