I updated to the current HEAD (72384b0a1f37636c879e6f499785fb4e1292ee91), and now I'm getting:
[value] Analyzing a complete application starting at main
[value] Computing initial state
[kernel] Current source was: mkfs_server.c:10
The full backtrace is:
Raised at file "src/plugins/value/values/cvalue_forward.ml", line 300, characters 2-14
Called from file "src/plugins/value/values/cvalue_forward.ml", line 303, characters 20-76
Called from file "src/plugins/value/values/main_values.ml", line 84, characters 8-66
Called from file "src/plugins/value/engine/evaluation.ml", line 444, characters 14-58
Called from file "src/plugins/value/eval.ml", line 49, characters 29-32
Called from file "src/plugins/value/eval.ml", line 49, characters 29-32
Called from file "src/plugins/value/engine/evaluation.ml", line 404, characters 4-42
Called from file "src/plugins/value/engine/evaluation.ml", line 361, characters 35-72
Called from file "src/plugins/value/engine/evaluation.ml", line 336, characters 6-54
Called from file "src/plugins/value/engine/evaluation.ml", line 441, characters 6-32
Called from file "src/plugins/value/engine/evaluation.ml", line 404, characters 4-42
Called from file "src/plugins/value/engine/evaluation.ml", line 361, characters 35-72
Called from file "src/plugins/value/engine/evaluation.ml", line 336, characters 6-54
Called from file "src/plugins/value/engine/evaluation.ml", line 448, characters 6-31
Called from file "src/plugins/value/engine/evaluation.ml", line 404, characters 4-42
Called from file "src/plugins/value/engine/evaluation.ml", line 361, characters 35-72
Called from file "src/plugins/value/engine/evaluation.ml", line 336, characters 6-54
Called from file "src/plugins/value/engine/evaluation.ml", line 946, characters 24-77
Called from file "src/plugins/value/engine/initialization.ml", line 120, characters 4-38
Called from file "src/plugins/value/eval.ml", line 49, characters 29-32
Called from file "src/plugins/value/engine/initialization.ml", line 127, characters 23-64
Called from file "list.ml", line 84, characters 24-34
Called from file "src/plugins/value/engine/initialization.ml", line 298, characters 22-51
Called from file "list.ml", line 84, characters 24-34
Called from file "src/kernel_services/ast_data/globals.ml", line 122, characters 33-72
Called from file "src/libraries/project/state_builder.ml", line 399, characters 17-21
Called from file "src/plugins/value/engine/compute_functions.ml", line 215, characters 48-71
Called from file "src/plugins/value/legacy/eval_funs.ml", line 263, characters 15-40
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/values/cvalue_forward.ml", line 300, characters 2-8: Assertion failed).
Please report at https://github.com/TrustInSoft/tis-interpreter/issues
pascal-cuoq
commented
8 years ago
I updated to the current HEAD (72384b0a1f37636c879e6f499785fb4e1292ee91), and now I'm getting:
mkfs_server.c is a file generated by tis-mkfs.
Reverting the last commit fixes the issue for me.