Merge branch 'feature/ghost/fix-vlas-and-builtins' into 'master'
[ghost] fix VLAs and builtins calls Closes #1173, #2580 et #918 See merge request frama-c/frama-c!3932
Showing
- share/libc/__fc_builtin.h 50 additions, 35 deletionsshare/libc/__fc_builtin.h
- src/kernel_internals/typing/cabs2cil.ml 7 additions, 0 deletionssrc/kernel_internals/typing/cabs2cil.ml
- src/kernel_internals/typing/ghost_accesses.ml 14 additions, 9 deletionssrc/kernel_internals/typing/ghost_accesses.ml
- src/plugins/aorai/tests/ya/oracle/serial.res.oracle 1 addition, 185 deletionssrc/plugins/aorai/tests/ya/oracle/serial.res.oracle
- src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle 1 addition, 1 deletionsrc/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
- src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif 202 additions, 202 deletions...ugins/markdown-report/tests/sarif/oracle/std_string.sarif
- src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle 2 additions, 0 deletionssrc/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
- src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle 2 additions, 0 deletions...gins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle
- tests/libc/fc_builtins_in_ghost.c 7 additions, 0 deletionstests/libc/fc_builtins_in_ghost.c
- tests/libc/oracle/argz_c.res.oracle 1 addition, 0 deletionstests/libc/oracle/argz_c.res.oracle
- tests/libc/oracle/coverage.res.oracle 1 addition, 1 deletiontests/libc/oracle/coverage.res.oracle
- tests/libc/oracle/fc_builtins_in_ghost.res.oracle 20 additions, 0 deletionstests/libc/oracle/fc_builtins_in_ghost.res.oracle
- tests/libc/oracle/fc_libc.1.res.oracle 16 additions, 212 deletionstests/libc/oracle/fc_libc.1.res.oracle
- tests/libc/oracle/netdb_c.res.oracle 1 addition, 0 deletionstests/libc/oracle/netdb_c.res.oracle
- tests/syntax/ghost_vla.i 9 additions, 0 deletionstests/syntax/ghost_vla.i
- tests/syntax/oracle/ghost_vla.res.oracle 34 additions, 0 deletionstests/syntax/oracle/ghost_vla.res.oracle
Loading
Please register or sign in to comment