Skip to content
Snippets Groups Projects

sync with frama-c master; fix papabench's math.h inclusion

Merged Andre Maroneze requested to merge fix-papabench into master
24 files
+ 92
95
Compare changes
  • Side-by-side
  • Inline
Files
24
@@ -854,10 +854,10 @@ FRAMAC_SHARE/libc string.h 118 memset precondition Unknown valid_s: valid_or_emp
FRAMAC_SHARE/libc string.h 128 strlen precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc string.h 160 strchr precondition Unknown valid_string_s: valid_read_string(s)
FRAMAC_SHARE/libc unistd.h 774 chown precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 1116 unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc unistd.h 1123 unlink precondition Unknown valid_string_path: valid_read_string(path)
FRAMAC_SHARE/libc/sys stat.h 32 chmod assigns clause Unknown assigns \nothing;
FRAMAC_SHARE/libc/sys stat.h 32 chmod from clause Unknown assigns \result \from \nothing;
FRAMAC_SHARE/libc/sys stat.h 84 stat precondition Unknown valid_pathname: valid_read_string(pathname)
FRAMAC_SHARE/libc/sys stat.h 87 stat precondition Unknown valid_pathname: valid_read_string(pathname)
test/unit ntp_core.c 179 send_response precondition of __FC_assert Invalid or unreachable nonnull_c: c ≢ 0
test/unit ntp_core.c 186 send_response precondition of __FC_assert Unknown nonnull_c: c ≢ 0
test/unit ntp_core.c 192 send_response precondition of __FC_assert Invalid or unreachable nonnull_c: c ≢ 0
Loading