Skip to content
Snippets Groups Projects

Feature/new cgc

Open Dario Pinto requested to merge feature/new-cgc into master
Files
21
directory file line function property kind status property
CGC_LIB libcgc.c 28 cgc_transmit precondition of write Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
CGC_LIB libcgc.c 172 cgc_allocate precondition Invalid or unreachable valid_addr: \valid((char *)*addr)
FRAMAC_SHARE/libc unistd.h 1133 write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
src map.c 36 cgc_initMap precondition of cgc_allocate Invalid or unreachable valid_addr: \valid((char *)*addr)
src service.c 102 main initialization Unknown \initialized(&instruction)
src service.c 105 main initialization Unknown \initialized(&value)
src service.c 127 main initialization Unknown \initialized(&value)
src service.c 127 main signed_overflow Unknown budget - value ≤ 2147483647
Loading