From 1280368e2cbe329092ad6bccef089d72dce1bcbe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= <git@haerdin.se>
Date: Wed, 15 May 2024 20:06:36 +0200
Subject: [PATCH 2/7] eva: Add av_log2_16bit()

---
 libavutil/common.h | 3 +++
 libavutil/eva.c    | 2 ++
 2 files changed, 5 insertions(+)

diff --git a/libavutil/common.h b/libavutil/common.h
index b532ef8a46..d81131f8ad 100644
--- a/libavutil/common.h
+++ b/libavutil/common.h
@@ -167,6 +167,9 @@ av_const int av_log2(unsigned v);
 #endif
 
 #ifndef av_log2_16bit
+/*@ ensures 0 <= \result <= 15;
+    assigns \result \from v;
+ */
 av_const int av_log2_16bit(unsigned v);
 #endif
 
diff --git a/libavutil/eva.c b/libavutil/eva.c
index c7f0c9a09c..1f7f457015 100644
--- a/libavutil/eva.c
+++ b/libavutil/eva.c
@@ -3,6 +3,8 @@
 
 int main(void) {
     unsigned uint = Frama_C_unsigned_int_interval(0, UINT_MAX);
+    unsigned short ushort = Frama_C_unsigned_short_interval(0, UINT16_MAX);
     av_log2(uint);
+    av_log2_16bit(ushort);
     return 0;
 }
-- 
2.39.2