diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml index 3bf647bcaa472e030cd5ddb1868c4e77f8d504b4..74ea3ab799eddce2ab73093eea341864183ba3c1 100644 --- a/src/kernel_internals/typing/asm_contracts.ml +++ b/src/kernel_internals/typing/asm_contracts.ml @@ -138,8 +138,8 @@ object(self) let once = true in Kernel.warning ~once ~source - "Clobber list contain \"memory\" argument. Assuming no \ - side-effect beyond those mentioned in operands." + "Clobber list contains \"memory\" argument. Assuming no \ + side effects beyond those mentioned in operands." end; let to_id_term lv = Logic_const.new_identified_term diff --git a/tests/syntax/oracle/gnu-asm-aesni.res.oracle b/tests/syntax/oracle/gnu-asm-aesni.res.oracle index f5375b6410ba81211be14dda65908129e74c04c1..009db9d96ab42af2b72897a78f16ec0ba3ebadab 100644 --- a/tests/syntax/oracle/gnu-asm-aesni.res.oracle +++ b/tests/syntax/oracle/gnu-asm-aesni.res.oracle @@ -1,6 +1,6 @@ [kernel] Parsing tests/syntax/gnu-asm-aesni.c (with preprocessing) [kernel] tests/syntax/gnu-asm-aesni.c:93: Warning: - Clobber list contain "memory" argument. Assuming no side-effect beyond those mentioned in operands. + Clobber list contains "memory" argument. Assuming no side effects beyond those mentioned in operands. /* Generated by Frama-C */ #include "__fc_builtin.h" #include "string.h"