From b05dfc200bd125a04eddfac301f7b629858035cf Mon Sep 17 00:00:00 2001 From: Christophe Grenier Date: Sun, 8 Oct 2023 13:57:07 +0200 Subject: [PATCH] src/adv.c: add Frama-C annotation for interface_adv() --- src/adv.c | 1 + 1 file changed, 1 insertion(+) diff --git a/src/adv.c b/src/adv.c index 837c10ec..510b48fe 100644 --- a/src/adv.c +++ b/src/adv.c @@ -460,6 +460,7 @@ void interface_adv(disk_t *disk_car, const int verbose,const int dump_ind, const assert(current_cmd!=NULL); log_info("\nInterface Advanced\n"); list_part=disk_car->arch->read_part(disk_car,verbose,0); + /*@ assert valid_list_part(list_part); */ current_element=list_part; log_all_partitions(disk_car, list_part); while(1)