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
Viewing commit ff077078
Prev Next
Show latest version
23 files
+ 9190
− 0
Compare changes
  • Side-by-side
  • Inline
Files
23
cgc-challenges/Monster_Game/.frama-c/Monster_Game.eva/alarms.csv 0 → 100644
+ 146
− 0
directory file line function property kind status property
. service.c 75 cgc_check_egg index_bound Unknown eggindex < 10
. service.c 81 cgc_check_egg index_bound Unknown eggindex < 10
. service.c 83 cgc_check_egg dangling_pointer Unknown ¬\dangling(&pp->mons[0])
. service.c 83 cgc_check_egg mem_access Unknown \valid(&(pp->mons[0])->hitpoints)
. service.c 84 cgc_check_egg mem_access Unknown \valid(&(pp->mons[0])->health)
. service.c 85 cgc_check_egg mem_access Unknown \valid(&(pp->mons[0])->power)
. service.c 152 cgc_read_line_u mem_access Unknown \valid(outbuf + index_0)
. service.c 246 cgc_print_map precondition of bzero Unknown valid_memory_area: \valid((char *)s + (0 .. n - 1))
. service.c 250 cgc_print_map mem_access Unknown \valid(data + tmp)
. service.c 253 cgc_print_map initialization Unknown \initialized(pm->data + index_0)
. service.c 253 cgc_print_map mem_access Unknown \valid_read(pm->data + index_0)
. service.c 254 cgc_print_map mem_access Unknown \valid(data + map_index)
. service.c 256 cgc_print_map mem_access Unknown \valid(data + map_index)
. service.c 263 cgc_print_map mem_access Unknown \valid(data + map_index)
. service.c 265 cgc_print_map precondition of printf_va_12 Unknown valid_read_string(param0)
. service.c 265 printf_va_12 precondition Unknown valid_read_string(param0)
. service.c 277 cgc_find_path postcondition Unknown \result ≡ 0 ∨ \result ≡ 1
. service.c 346 cgc_place_marker mem_access Unknown \valid_read(secret_page + cgc_page_index)
. service.c 354 cgc_place_marker initialization Unknown \initialized(pm->data + index_0)
. service.c 354 cgc_place_marker mem_access Unknown \valid_read(pm->data + index_0)
. service.c 372 cgc_place_marker initialization Unknown \initialized(pm->data + index_0)
. service.c 372 cgc_place_marker mem_access Unknown \valid_read(pm->data + index_0)
. service.c 386 cgc_place_marker mem_access Unknown \valid(pm->data + index_0)
. service.c 395 cgc_set_marker mem_access Unknown \valid(pm->data + index_0)
. service.c 414 cgc_initialize_map precondition of bzero Unknown valid_memory_area: \valid((char *)s + (0 .. n - 1))
. service.c 425 cgc_initialize_map mem_access Unknown \valid_read(secret_page + cgc_page_index)
. service.c 463 cgc_initialize_queue_matrix precondition of bzero Unknown valid_memory_area: \valid((char *)s + (0 .. n - 1))
. service.c 467 cgc_initialize_queue_matrix initialization Unknown \initialized(pm->data + index_0)
. service.c 467 cgc_initialize_queue_matrix mem_access Unknown \valid_read(pm->data + index_0)
. service.c 468 cgc_initialize_queue_matrix mem_access Unknown \valid(queue_matrix + index_0)
. service.c 512 cgc_generate_map mem_access Unknown \valid(pm->data + (unsigned int)((unsigned int)(pm->width * pm->last_y) + pm->last_x))
. service.c 551 cgc_select_monster dangling_pointer Unknown ¬\dangling(&pp->mons[index_0])
. service.c 551 cgc_select_monster initialization Unknown \initialized(&(pp->mons[index_0])->health)
. service.c 551 cgc_select_monster mem_access Unknown \valid_read(&(pp->mons[index_0])->health)
. service.c 565 cgc_select_monster initialization Unknown \initialized(&(pp->mons[index_0])->type)
. service.c 565 cgc_select_monster mem_access Unknown \valid_read(&(pp->mons[index_0])->type)
. service.c 565 cgc_select_monster precondition of printf_va_21 Unknown valid_read_string(param0)
. service.c 565 printf_va_21 precondition Unknown valid_read_string(param0)
. service.c 566 cgc_select_monster initialization Unknown \initialized(&(pp->mons[index_0])->level)
. service.c 566 cgc_select_monster mem_access Unknown \valid_read(&(pp->mons[index_0])->level)
. service.c 567 cgc_select_monster initialization Unknown \initialized(&(pp->mons[index_0])->health)
. service.c 568 cgc_select_monster initialization Unknown \initialized(&(pp->mons[index_0])->power)
. service.c 581 cgc_select_monster dangling_pointer Unknown ¬\dangling(&pp->mons[(int)(ac - 1)])
. service.c 583 cgc_select_monster initialization Unknown \initialized(&(pp->mons[(int)(ac - 1)])->health)
. service.c 583 cgc_select_monster mem_access Unknown \valid_read(&(pp->mons[(int)(ac - 1)])->health)
. service.c 590 cgc_select_monster dangling_pointer Unknown ¬\dangling(&pp->mons[(int)(ac - 1)])
. service.c 590 cgc_select_monster index_bound Unknown (int)(ac - 1) < 5
. service.c 590 cgc_select_monster index_bound Unknown 0 ≤ (int)(ac - 1)
. service.c 590 cgc_select_monster signed_overflow Unknown -2147483648 ≤ ac - 1
. service.c 603 cgc_reset_monsters dangling_pointer Unknown ¬\dangling(&pp->mons[index_0])
. service.c 603 cgc_reset_monsters initialization Unknown \initialized(&(pp->mons[index_0])->hitpoints)
. service.c 603 cgc_reset_monsters mem_access Unknown \valid(&(pp->mons[index_0])->health)
. service.c 603 cgc_reset_monsters mem_access Unknown \valid_read(&(pp->mons[index_0])->hitpoints)
. service.c 616 cgc_print_monster initialization Unknown \initialized(&pm->type)
. service.c 616 cgc_print_monster mem_access Unknown \valid_read(&pm->type)
. service.c 616 cgc_print_monster precondition of printf_va_29 Unknown valid_read_string(param0)
. service.c 616 printf_va_29 precondition Unknown valid_read_string(param0)
. service.c 617 cgc_print_monster initialization Unknown \initialized(&pm->level)
. service.c 617 cgc_print_monster mem_access Unknown \valid_read(&pm->level)
. service.c 618 cgc_print_monster initialization Unknown \initialized(&pm->health)
. service.c 619 cgc_print_monster initialization Unknown \initialized(&pm->hitpoints)
. service.c 620 cgc_print_monster initialization Unknown \initialized(&pm->power)
. service.c 631 cgc_oneup_monster initialization Unknown \initialized(&pm->experience)
. service.c 631 cgc_oneup_monster mem_access Unknown \valid(&pm->experience)
. service.c 634 cgc_oneup_monster initialization Unknown \initialized(&pm->type)
. service.c 634 cgc_oneup_monster mem_access Unknown \valid_read(&pm->type)
. service.c 634 cgc_oneup_monster precondition of printf_va_34 Unknown valid_read_string(param0)
. service.c 634 printf_va_34 precondition Unknown valid_read_string(param0)
. service.c 635 cgc_oneup_monster initialization Unknown \initialized(&pm->hitpoints)
. service.c 636 cgc_oneup_monster initialization Unknown \initialized(&pm->power)
. service.c 637 cgc_oneup_monster initialization Unknown \initialized(&pm->hitpoints)
. service.c 638 cgc_oneup_monster initialization Unknown \initialized(&pm->level)
. service.c 638 cgc_oneup_monster mem_access Unknown \valid(&pm->level)
. service.c 697 cgc_change_monster_name precondition of bzero Unknown valid_memory_area: \valid((char *)s + (0 .. n - 1))
. service.c 698 cgc_change_monster_name precondition of memcpy Unknown valid_dest: valid_or_empty(dest, n)
. service.c 698 cgc_change_monster_name precondition of memcpy Unknown valid_src: valid_read_or_empty(src, n)
. service.c 741 cgc_capture_boss dangling_pointer Unknown ¬\dangling(&pp->mons[choice])
. service.c 746 cgc_capture_boss initialization Unknown \initialized(&pm->hitpoints)
. service.c 771 cgc_capture_boss precondition of free Unknown freeable: p ≡ \null ∨ \freeable(p)
. service.c 772 cgc_capture_boss dangling_pointer Unknown ¬\dangling(&pm)
. service.c 795 cgc_daboss initialization Unknown \initialized(&boss->health)
. service.c 803 cgc_daboss initialization Unknown \initialized(&player_current->power)
. service.c 803 cgc_daboss mem_access Unknown \valid_read(&player_current->power)
. service.c 803 cgc_daboss division_by_zero Unknown player_current->power ≢ 0
. service.c 811 cgc_daboss initialization Unknown \initialized(&boss->health)
. service.c 818 cgc_daboss initialization Unknown \initialized(&boss->power)
. service.c 818 cgc_daboss division_by_zero Unknown boss->power ≢ 0
. service.c 821 cgc_daboss initialization Unknown \initialized(&boss->type)
. service.c 821 cgc_daboss initialization Unknown \initialized(&player_current->type)
. service.c 821 cgc_daboss mem_access Unknown \valid_read(&player_current->type)
. service.c 821 cgc_daboss precondition of printf_va_52 Unknown valid_read_string(param0)
. service.c 821 cgc_daboss precondition of printf_va_52 Unknown valid_read_string(param1)
. service.c 821 printf_va_52 precondition Unknown valid_read_string(param0)
. service.c 821 printf_va_52 precondition Unknown valid_read_string(param1)
. service.c 823 cgc_daboss initialization Unknown \initialized(&player_current->health)
. service.c 826 cgc_daboss initialization Unknown \initialized(&player_current->type)
. service.c 826 cgc_daboss precondition of printf_va_53 Unknown valid_read_string(param0)
. service.c 826 printf_va_53 precondition Unknown valid_read_string(param0)
. service.c 861 cgc_capture_monster dangling_pointer Unknown ¬\dangling(&pp->mons[choice])
. service.c 890 cgc_capture_monster precondition of free Unknown freeable: p ≡ \null ∨ \freeable(p)
. service.c 891 cgc_capture_monster dangling_pointer Unknown ¬\dangling(&pm)
. service.c 915 cgc_fight initialization Unknown \initialized(&pm->health)
. service.c 923 cgc_fight initialization Unknown \initialized(&player_current->power)
. service.c 923 cgc_fight mem_access Unknown \valid_read(&player_current->power)
. service.c 923 cgc_fight division_by_zero Unknown player_current->power ≢ 0
. service.c 931 cgc_fight initialization Unknown \initialized(&pm->health)
. service.c 932 cgc_fight initialization Unknown \initialized(&pm->type)
. service.c 932 cgc_fight precondition of printf_va_65 Unknown valid_read_string(param0)
. service.c 932 printf_va_65 precondition Unknown valid_read_string(param0)
. service.c 938 cgc_fight initialization Unknown \initialized(&pm->power)
. service.c 938 cgc_fight division_by_zero Unknown pm->power ≢ 0
. service.c 941 cgc_fight initialization Unknown \initialized(&player_current->type)
. service.c 941 cgc_fight initialization Unknown \initialized(&pm->type)
. service.c 941 cgc_fight mem_access Unknown \valid_read(&player_current->type)
. service.c 941 cgc_fight precondition of printf_va_66 Unknown valid_read_string(param0)
. service.c 941 cgc_fight precondition of printf_va_66 Unknown valid_read_string(param1)
. service.c 941 printf_va_66 precondition Unknown valid_read_string(param0)
. service.c 941 printf_va_66 precondition Unknown valid_read_string(param1)
. service.c 943 cgc_fight initialization Unknown \initialized(&player_current->health)
. service.c 946 cgc_fight initialization Unknown \initialized(&player_current->type)
. service.c 946 cgc_fight precondition of printf_va_67 Unknown valid_read_string(param0)
. service.c 946 printf_va_67 precondition Unknown valid_read_string(param0)
. service.c 982 cgc_movement_loop initialization Unknown \initialized(pm->data + (unsigned int)((unsigned int)(pm->width * (unsigned int)(pm->current_y - 1)) + pm->current_x))
. service.c 982 cgc_movement_loop mem_access Unknown \valid_read(pm->data + (unsigned int)((unsigned int)(pm->width * (unsigned int)(pm->current_y - 1)) + pm->current_x))
. service.c 993 cgc_movement_loop initialization Unknown \initialized(pm->data + (unsigned int)((unsigned int)(pm->width * (unsigned int)(pm->current_y + 1)) + pm->current_x))
. service.c 993 cgc_movement_loop mem_access Unknown \valid_read(pm->data + (unsigned int)((unsigned int)(pm->width * (unsigned int)(pm->current_y + 1)) + pm->current_x))
. service.c 1004 cgc_movement_loop initialization Unknown \initialized(pm->data + (unsigned int)((unsigned int)((unsigned int)(pm->width * pm->current_y) + pm->current_x) - 1))
. service.c 1004 cgc_movement_loop mem_access Unknown \valid_read(pm->data + (unsigned int)((unsigned int)((unsigned int)(pm->width * pm->current_y) + pm->current_x) - 1))
. service.c 1015 cgc_movement_loop initialization Unknown \initialized(pm->data + (unsigned int)((unsigned int)((unsigned int)(pm->width * pm->current_y) + pm->current_x) + 1))
. service.c 1015 cgc_movement_loop mem_access Unknown \valid_read(pm->data + (unsigned int)((unsigned int)((unsigned int)(pm->width * pm->current_y) + pm->current_x) + 1))
. service.c 1072 cgc_select_name index_bound Unknown index_0 < 47
. service.c 1141 cgc_generate_player index_bound Unknown tmp < 5
. service.c 1162 cgc_print_player initialization Unknown \initialized(&(pp->mons[index_0])->type)
. service.c 1162 cgc_print_player mem_access Unknown \valid_read(&(pp->mons[index_0])->type)
. service.c 1162 cgc_print_player precondition of printf_va_89 Unknown valid_read_string(param0)
. service.c 1162 printf_va_89 precondition Unknown valid_read_string(param0)
. service.c 1162 cgc_print_player index_bound Unknown index_0 < 5
. service.c 1163 cgc_print_player initialization Unknown \initialized(&(pp->mons[index_0])->health)
. service.c 1163 cgc_print_player mem_access Unknown \valid_read(&(pp->mons[index_0])->health)
. service.c 1164 cgc_print_player initialization Unknown \initialized(&(pp->mons[index_0])->power)
. service.c 1164 cgc_print_player mem_access Unknown \valid_read(&(pp->mons[index_0])->power)
FRAMAC_SHARE/libc stdlib.h 405 free precondition Unknown freeable: p ≡ \null ∨ \freeable(p)
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 strings.h 36 bzero precondition Unknown valid_memory_area: \valid((char *)s + (0 .. n - 1))