问题标签 [compcert]

我在 Coq 的规范文件中有以下定义。我需要一个比较两个“int”类型值的命题。这两个是 't' 和 'Int.repr (i.(period1))'。(i.period1) 和 (i.period2) 具有类型 'Z'。

这是我的代码片段：

这给了我以下错误：

术语“t”的类型为“int”，而预期的类型为“Z”。

我也试过：

但它给了我这个错误：

术语“Int.cmpu Cgt t (Int.repr (period1 i))”具有“bool”类型，而预期具有“Prop”类型。

有什么方法可以比较这两种“int”类型或将它们转换为其他类型并返回“prop”类型？

谢谢，

我有以下引理，但无法证明：

我找到了平等的策略（链接），但找不到 lt/ltu 或 gt/gtu 的策略：

任何帮助将不胜感激！

谢谢，

我怎样才能证明这两个陈述是相等的：

1. Val.shru (Val.and a (Vint b)) (Vint c) = Vint ?3434 /\ ?3434 <> d

2. Val.shru (Val.and a (Vint b)) (Vint c) <> d

这个概念非常简单，但停留在寻找解决它的正确策略上。这实际上是我要证明的引理：

谢谢，

我正在证明这个引理：

我尝试过展开not, Val.cmp, ...和使用rewrite，H但没有去任何地方。任何帮助表示赞赏。

谢谢

我有定义my_def1：

我想写另一个my_def2类似于下面的定义并添加一个总是返回my_def1的公理，所以：proj_bytes vlSome bl

我的问题是我怎样才能完成my_def2和写相axiom​​关的proj_bytes vl？

或者问题是如何从类型list memval转换为 list byte[decode_int接受list byte]？

这是 的定义memval：

我正在尝试展开 Mem.load 并收到错误消息：

错误：无法强制Mem.load转换为可评估的参考。

我写的和 as 完全一样，Definition而且是可展开的。Mem.loadload1

我想证明一个小于 Int.max_unsigned 的 Z 类型值。

引理检验：10%Z < Int.max_unsigned。证明。?? 如何证明上述测试引理？

EvalOp 的定义在compcert.backend.SplitLongproof：

这个定义的奇怪之处在于将andcoqdoc --html识别为两个单独的标记：EvalOp

为什么 Coq 允许在中间没有分隔符（空格）的两个标记？或者这是一个错误coqdoc？感谢您的帮助！

我正在按照此处的说明安装 CompCert C 编译器：https ://compcert.org/man/manual002.html 。

但是，我陷入了“使​​用适当的选项运行配置脚本：./configure [option ...] target”的阶段

控制台输出为：

我正在运行 Ubuntu 20.04 LTS。

[编辑：我设法运行了 ./configure。但是我无法重现我如何做到的确切方法。现在我陷入了不同的境地。]

后续问题：

运行时，make all我收到以下输出：

我通过复制lib/Axiom.v到根目录解决了这个问题。然后make all抱怨另一个库，lib/所以我移动了一堆，直到收到以下错误：

现在我又被困住了。

CompCert手册在 §6.5.2 中说明

如果在将值存储在对象的不同成员中之后访问联合对象的成员，则行为如上面最后一段所述：只要不需要访问存储的指针，该操作就被很好地定义了指针类型以外的类型或与指针类型大小相同的整数类型的值。例如，声明...

...支持在存储任何其他成员后访问任何成员。

所以我认为，在这个例子中，存储后的fprinting是定义的行为。但我仍然不知道这种行为实际上是什么。它会简单地保留 的字节表示，但尝试将其内容显示为' 类型吗？会吗？编译器会像除以零一样优化它吗？u.cu.du.du.cnull