From 919279c36ee2bf93e02a756148eb8316e1a535a1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= Date: Wed, 15 May 2024 20:01:48 +0200 Subject: [PATCH 1/7] lavu: Very basic Eva setup Only av_log2() for now. --- libavutil/Makefile | 8 ++++++++ libavutil/common.h | 7 +++++-- libavutil/eva.c | 8 ++++++++ 3 files changed, 21 insertions(+), 2 deletions(-) create mode 100644 libavutil/eva.c diff --git a/libavutil/Makefile b/libavutil/Makefile index 6e6fa8d800..d9c59f02c7 100644 --- a/libavutil/Makefile +++ b/libavutil/Makefile @@ -290,3 +290,11 @@ tools/crypto_bench$(EXESUF): ELIBS += $(if $(VERSUS),$(subst +, -l,+$(VERSUS)),) tools/crypto_bench.o: CFLAGS += -DUSE_EXT_LIBS=0$(if $(VERSUS),$(subst +,+USE_,+$(VERSUS)),) $(SUBDIR)tests/lzo$(EXESUF): ELIBS = -llzo2 + +verify: + frama-c -cpp-extra-args="-DEVA -I.." -eva eva.c + +verify-gui: + frama-c-gui -cpp-extra-args="-DEVA -I.." -eva eva.c + +.PHONY: verify diff --git a/libavutil/common.h b/libavutil/common.h index 3e4c339893..b532ef8a46 100644 --- a/libavutil/common.h +++ b/libavutil/common.h @@ -160,6 +160,9 @@ #endif #ifndef av_log2 +/*@ ensures 0 <= \result <= 31; + assigns \result \from v; + */ av_const int av_log2(unsigned v); #endif @@ -349,7 +352,7 @@ static av_always_inline int av_sat_dsub32_c(int a, int b) * @return sum with signed saturation */ static av_always_inline int64_t av_sat_add64_c(int64_t a, int64_t b) { -#if (!defined(__INTEL_COMPILER) && AV_GCC_VERSION_AT_LEAST(5,1)) || AV_HAS_BUILTIN(__builtin_add_overflow) +#if (!defined(__INTEL_COMPILER) && AV_GCC_VERSION_AT_LEAST(5,1) && !defined(EVA)) || AV_HAS_BUILTIN(__builtin_add_overflow) int64_t tmp; return !__builtin_add_overflow(a, b, &tmp) ? tmp : (tmp < 0 ? INT64_MAX : INT64_MIN); #else @@ -368,7 +371,7 @@ static av_always_inline int64_t av_sat_add64_c(int64_t a, int64_t b) { * @return difference with signed saturation */ static av_always_inline int64_t av_sat_sub64_c(int64_t a, int64_t b) { -#if (!defined(__INTEL_COMPILER) && AV_GCC_VERSION_AT_LEAST(5,1)) || AV_HAS_BUILTIN(__builtin_sub_overflow) +#if (!defined(__INTEL_COMPILER) && AV_GCC_VERSION_AT_LEAST(5,1) && !defined(EVA)) || AV_HAS_BUILTIN(__builtin_sub_overflow) int64_t tmp; return !__builtin_sub_overflow(a, b, &tmp) ? tmp : (tmp < 0 ? INT64_MAX : INT64_MIN); #else diff --git a/libavutil/eva.c b/libavutil/eva.c new file mode 100644 index 0000000000..c7f0c9a09c --- /dev/null +++ b/libavutil/eva.c @@ -0,0 +1,8 @@ +#include "common.h" +#include "__fc_builtin.h" + +int main(void) { + unsigned uint = Frama_C_unsigned_int_interval(0, UINT_MAX); + av_log2(uint); + return 0; +} -- 2.39.2