From 16ec8ee8b5c2d273e16b53fe94cad9c5e54f31ff Mon Sep 17 00:00:00 2001
From: Christophe Grenier <grenier@cgsecurity.org>
Date: Sun, 1 Nov 2020 13:27:37 +0100
Subject: [PATCH] src/file_ab.c: fix frama-c annotation

---
 src/file_ab.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/file_ab.c b/src/file_ab.c
index 011e6757..af922527 100644
--- a/src/file_ab.c
+++ b/src/file_ab.c
@@ -52,7 +52,7 @@ struct ab_header
   @ requires (buffer_size&1)==0;
   @ requires \valid_read(buffer+(0..buffer_size-1));
   @ requires \valid(file_recovery);
-  @ requires file_recovery->data_check==&data_check_ab;
+  @ requires file_recovery->data_check==&data_check_addressbook;
   @ requires \separated(buffer, file_recovery);
   @ ensures \result == DC_CONTINUE || \result == DC_STOP;
   @ assigns file_recovery->calculated_file_size;