Skip to content
Snippets Groups Projects

Feature/new cgc

Open Feature/new cgc
feature/new-cgc into master
Open Dario Pinto requested to merge feature/new-cgc into master
Compare
and
Show latest version
20 files
+ 397
− 461
Compare changes
  • Side-by-side
  • Inline
Files
20
cgc-challenges/3D_Image_Toolkit/.frama-c/3D_Image_Toolkit.eva/alarms.csv 0 → 100644
+ 117
− 0
directory file line function property kind status property
. 3dc.c 44 cgc_Push precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. 3dc.c 47 cgc_Push initialization Unknown \initialized(px_list_0 + i)
. 3dc.c 47 cgc_Push mem_access Unknown \valid_read(px_list_0 + i)
. 3dc.c 61 cgc_RunTask initialization Unknown \initialized(px_list_0 + tmp)
. 3dc.c 61 cgc_RunTask mem_access Unknown \valid_read(px_list_0 + tmp)
. 3dc.c 78 cgc_ReadFile mem_access Unknown \valid(&px->x)
. 3dc.c 105 cgc_NewFile initialization Unknown \initialized(px_list_0 + tmp_0)
. 3dc.c 105 cgc_NewFile mem_access Unknown \valid_read(px_list_0 + tmp_0)
. 3dc.c 107 cgc_NewFile precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. 3dc.c 110 cgc_NewFile precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. 3dc.c 113 cgc_NewFile precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. 3dc.c 116 cgc_NewFile precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. 3dc.c 119 cgc_NewFile precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. 3dc.c 122 cgc_NewFile precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. 3dc.c 125 cgc_NewFile precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. 3dc.c 136 cgc_ShowPixel initialization Unknown \initialized(&px->x)
. 3dc.c 136 cgc_ShowPixel initialization Unknown \initialized(&px->y)
. 3dc.c 136 cgc_ShowPixel initialization Unknown \initialized(&px->z)
. 3dc.c 136 cgc_ShowPixel mem_access Unknown \valid_read(&px->z)
. 3dc.c 137 cgc_ShowPixel initialization Unknown \initialized(&px->a)
. 3dc.c 137 cgc_ShowPixel initialization Unknown \initialized(&px->b)
. 3dc.c 137 cgc_ShowPixel initialization Unknown \initialized(&px->g)
. 3dc.c 137 cgc_ShowPixel initialization Unknown \initialized(&px->r)
. 3dc.c 149 cgc_CheckFile initialization Unknown \initialized(&(*(px + i))->x)
. 3dc.c 149 cgc_CheckFile initialization Unknown \initialized(&(*(px + i))->y)
. 3dc.c 149 cgc_CheckFile initialization Unknown \initialized(&(*(px + i))->z)
. 3dc.c 149 cgc_CheckFile initialization Unknown \initialized(px + i)
. 3dc.c 149 cgc_CheckFile mem_access Unknown \valid_read(&(*(px + i))->z)
. 3dc.c 150 cgc_CheckFile initialization Unknown \initialized(&(*(px + i))->a)
. 3dc.c 150 cgc_CheckFile initialization Unknown \initialized(&(*(px + i))->b)
. 3dc.c 150 cgc_CheckFile initialization Unknown \initialized(&(*(px + i))->g)
. 3dc.c 150 cgc_CheckFile initialization Unknown \initialized(&(*(px + i))->r)
. 3dc.c 150 cgc_CheckFile mem_access Unknown \valid_read(&(*(px + i))->a)
. 3dc.c 161 cgc_RotateX initialization Unknown \initialized(&px->y)
. 3dc.c 161 cgc_RotateX mem_access Unknown \valid_read(&px->y)
. 3dc.c 161 cgc_RotateX initialization Unknown \initialized(&px->z)
. 3dc.c 162 cgc_RotateX initialization Unknown \initialized(&px->y)
. 3dc.c 170 cgc_RotateY initialization Unknown \initialized(&px->z)
. 3dc.c 170 cgc_RotateY mem_access Unknown \valid_read(&px->z)
. 3dc.c 170 cgc_RotateY initialization Unknown \initialized(&px->x)
. 3dc.c 171 cgc_RotateY initialization Unknown \initialized(&px->x)
. 3dc.c 179 cgc_RotateZ initialization Unknown \initialized(&px->x)
. 3dc.c 179 cgc_RotateZ mem_access Unknown \valid_read(&px->x)
. 3dc.c 179 cgc_RotateZ initialization Unknown \initialized(&px->y)
. 3dc.c 180 cgc_RotateZ initialization Unknown \initialized(&px->x)
. 3dc.c 186 cgc_SkewX initialization Unknown \initialized(&px->x)
. 3dc.c 186 cgc_SkewX mem_access Unknown \valid(&px->x)
. 3dc.c 190 cgc_SkewY initialization Unknown \initialized(&px->y)
. 3dc.c 190 cgc_SkewY mem_access Unknown \valid(&px->y)
. 3dc.c 194 cgc_SkewZ initialization Unknown \initialized(&px->z)
. 3dc.c 194 cgc_SkewZ mem_access Unknown \valid(&px->z)
. 3dc.c 206 cgc_Scale initialization Unknown \initialized(&px->x)
. 3dc.c 206 cgc_Scale mem_access Unknown \valid_read(&px->x)
. 3dc.c 207 cgc_Scale initialization Unknown \initialized(&px->y)
. 3dc.c 208 cgc_Scale initialization Unknown \initialized(&px->z)
. 3dc.c 250 cgc_Brightness initialization Unknown \initialized(&px->r)
. 3dc.c 250 cgc_Brightness mem_access Unknown \valid_read(&px->r)
. 3dc.c 251 cgc_Brightness initialization Unknown \initialized(&px->g)
. 3dc.c 252 cgc_Brightness initialization Unknown \initialized(&px->b)
. 3dc.c 284 cgc_Opacity mem_access Unknown \valid(&px->a)
. compress.c 83 cgc_Compress initialization Unknown \initialized(px_list_0 + tmp)
. compress.c 83 cgc_Compress mem_access Unknown \valid_read(px_list_0 + tmp)
. compress.c 83 cgc_Compress signed_overflow Unknown p_idx + 1 ≤ 2147483647
. compress.c 85 cgc_Compress initialization Unknown \initialized(&px->r)
. compress.c 85 cgc_Compress mem_access Unknown \valid_read(&px->r)
. compress.c 88 cgc_Compress initialization Unknown \initialized(&px->g)
. compress.c 91 cgc_Compress initialization Unknown \initialized(&px->b)
. compress.c 93 cgc_Compress precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. compress.c 96 cgc_Compress precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. compress.c 99 cgc_Compress precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. compress.c 102 cgc_Compress precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. compress.c 121 cgc_Decompress precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. compress.c 121 cgc_Decompress precondition of memcpy Unknown valid_src: valid_read_or_empty(src, n)
. compress.c 125 cgc_Decompress precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. compress.c 125 cgc_Decompress precondition of memcpy Unknown valid_src: valid_read_or_empty(src, n)
. compress.c 129 cgc_Decompress precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. compress.c 129 cgc_Decompress precondition of memcpy Unknown valid_src: valid_read_or_empty(src, n)
. compress.c 133 cgc_Decompress initialization Unknown \initialized(in_data + tmp)
. compress.c 133 cgc_Decompress mem_access Unknown \valid_read(in_data + tmp)
. compress.c 144 cgc_Decompress mem_access Unknown \valid(out_data + tmp_0)
. compress.c 145 cgc_Decompress mem_access Unknown \valid(out_data + tmp_1)
. compress.c 146 cgc_Decompress mem_access Unknown \valid(out_data + tmp_2)
. compress.c 148 cgc_Decompress mem_access Unknown \valid(out_data + tmp_3)
. compress.c 169 cgc_WriteOut initialization Unknown \initialized(px_list_0 + i)
. compress.c 169 cgc_WriteOut mem_access Unknown \valid_read(px_list_0 + i)
. compress.c 173 cgc_WriteOut precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. compress.c 173 cgc_WriteOut precondition of memcpy Unknown valid_src: valid_read_or_empty(src, n)
. compress.c 175 cgc_WriteOut precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. compress.c 175 cgc_WriteOut precondition of memcpy Unknown valid_src: valid_read_or_empty(src, n)
. compress.c 177 cgc_WriteOut precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. compress.c 177 cgc_WriteOut precondition of memcpy Unknown valid_src: valid_read_or_empty(src, n)
. compress.c 179 cgc_WriteOut mem_access Unknown \valid(&tmp->a)
. main.c 80 cgc_menu precondition of memset Unknown valid_s: valid_or_empty(s, n)
. main.c 107 cgc_menu initialization Unknown \initialized(&coord)
. main.c 109 cgc_menu initialization Unknown \initialized(&val)
. main.c 112 cgc_menu initialization Unknown \initialized(&val)
. main.c 115 cgc_menu initialization Unknown \initialized(&val)
. main.c 128 cgc_menu initialization Unknown \initialized(&coord)
. main.c 130 cgc_menu initialization Unknown \initialized(&val)
. main.c 133 cgc_menu initialization Unknown \initialized(&val)
. main.c 136 cgc_menu initialization Unknown \initialized(&val)
. main.c 148 cgc_menu initialization Unknown \initialized(&val)
. main.c 155 cgc_menu initialization Unknown \initialized(&val)
. main.c 162 cgc_menu initialization Unknown \initialized(&val)
. main.c 185 cgc_menu precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. main.c 185 cgc_menu precondition of memcpy Unknown valid_src: valid_read_or_empty(src, n)
. main.c 197 cgc_menu initialization Unknown \initialized(&val)
. main.c 200 cgc_menu initialization Unknown \initialized(px_list_0 + val)
. main.c 200 cgc_menu mem_access Unknown \valid_read(px_list_0 + val)
. main.c 200 cgc_menu precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. main.c 200 cgc_menu precondition of memcpy Unknown valid_src: valid_read_or_empty(src, n)
CGC_LIB libcgc.c 41 cgc_receive precondition of read Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc string.h 92 memcpy precondition Unknown valid_dest: valid_or_empty(dest, n)
FRAMAC_SHARE/libc string.h 93 memcpy precondition Unknown valid_src: valid_read_or_empty(src, n)
FRAMAC_SHARE/libc string.h 115 memset precondition Unknown valid_s: valid_or_empty(s, n)
FRAMAC_SHARE/libc unistd.h 1005 read precondition Unknown buf_has_room: \valid((char *)buf + (0 .. count - 1))