- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我已经尝试搜索文档和代码,但我无法找到这是什么以及如何更正它。
场景:
我正在使用 Ada SPARK 向量库并且我有以下代码:
package MyPackage
with SPARK_Mode => On
is
package New_Vectors is new Formal_Vectors (Index_Type => test, Element_Type => My_Element.Object);
type Object is private;
private
type Object is
record
Data : New_Vectors.Vector (Block_Vectors.Last_Count);
Identifier : Identifier_Range;
end record;
代码调用时出现错误:
function Make (Identifier : Identifier_Range) return Object is
begin
return (
Data => New_Vectors.Empty_Vector,
Identifier => Identifier);
end Make;
指向 Empty_Vector
。困难在于 Empty_Vector
将 Capacity
定义为 0
,这似乎是导致问题的原因。现在我不确定如何处理它,因为 Capacity
似乎在类型定义中(查看了 a-cofove.ads
)。
所以基本上我不知道如何解决这个问题;或者如何在未来发现这种情况。
最佳答案
您的分析是正确的。发生错误是因为您试图将空向量(即容量为 0 的向量)分配给容量为 Block_Vectors.Last_Count
的向量。 (这似乎是非零的)。
您实际上不需要为了使用它而显式初始化向量。默认初始化(使用 <>
,例如参见 here )就足够了,如下面的示例所示。
但是,为了证明不存在运行时错误,您确实需要使用Clear
显式清除向量. Empty_Vector
然后可以在断言中使用函数来检查向量是否为空,如下例所示。使用 gnatprove
可以证明该示例没有运行时错误.例如,在 GNAT Studio 中通过菜单 SPARK > Prove 打开证明设置,在“常规”部分(左上角)中选择“报告检查已移动”,然后通过选择“执行”(右下角)运行分析。
main.adb
with Ada.Text_IO; use Ada.Text_IO;
with Ada.Containers.Formal_Vectors;
procedure Main with SPARK_Mode is
package My_Vectors is new Ada.Containers.Formal_Vectors
(Index_Type => Natural,
Element_Type => Integer);
use My_Vectors;
type Object is record
Data : Vector (Capacity => 10); -- Max. # of elements: 10
Value : Integer;
end record;
-- Initialize with default value (i.e. <>), no explicit initialization needed.
Obj : Object :=
(Data => <>,
Value => 42);
begin
-- Clear the vector, required for the assertions to be proven.
Clear (Obj.Data);
-- Assert that the vector is not empty.
pragma Assert (Obj.Data = Empty_Vector);
-- Populate the vector with some elements.
Append (Obj.Data, 4);
Append (Obj.Data, 5);
Append (Obj.Data, 6);
-- Assert that the vector is populated.
pragma Assert (Obj.Data /= Empty_Vector);
-- Show the contents of Obj.Data.
Put_Line ("Contents of Obj.Data:");
for I in Natural range 0 .. Natural (Length (Obj.Data)) - 1 loop
Put_Line ("[" & I'Image & "]" & Element (Obj.Data, I)'Image);
end loop;
New_Line;
-- or, alternatively using an iterator ...
declare
I : Extended_Index := Iter_First (Obj.Data);
begin
while Iter_Has_Element (Obj.Data, I) loop
Put_Line ("[" & I'Image & "]" & Element (Obj.Data, I)'Image);
I := Iter_Next (Obj.Data, I);
end loop;
end;
New_Line;
-- Show the contents of Obj.Value.
Put_Line ("Contents of Obj.Value:");
Put_Line (Obj.Value'Image);
New_Line;
end Main;
输出
Contents of Obj.Data:
[ 0] 4
[ 1] 5
[ 2] 6
[ 0] 4
[ 1] 5
[ 2] 6
Contents of Obj.Value:
42
关于Ada constraint error : Discriminant check failed. 什么意思?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/65813267/
reqwest v0.9 将 serde v1.0 作为依赖项,因此实现 converting serde_json errors into reqwest error . 在我的代码中,我使用 se
我有这个代码: let file = FileStorage { // ... }; file.write("Test", bytes.as_ref()) .map_err(|e| Mu
我只是尝试用angular-cli创建一个新项目,然后运行服务器,但是它停止并显示一条有趣的消息:Error: No errors。 我以这种方式更新了(希望有帮助):npm uninstall -g
我从我的 javascript 发送交易 Metamask 打开传输对话框 我确定 i get an error message in metamask (inpage.js:1 MetaMask -
这个问题在这里已经有了答案: How do you define custom `Error` types in Rust? (3 个答案) How to get a reference to a
我想知道两者之间有什么大的区别 if let error = error{} vs if error != nil?或者只是人们的不同之处,比如他们如何用代码表达自己? 例如,如果我使用这段代码: u
当我尝试发送超过 50KB 的图像时,我在 Blazor 服务器应用程序上收到以下错误消息 Error: Connection disconnected with error 'Error: Serv
我有一个error-page指令,它将所有异常重定向到错误显示页面 我的web.xml: [...] java.lang.Exception /vi
我有这样的对象: address: { "phone" : 888, "value" : 12 } 在 WHERE 中我需要通过 address.value 查找对象,但是在 SQL 中有函数
每次我尝试编译我的代码时,我都会遇到大量错误。这不是我的代码的问题,因为它在另一台计算机上工作得很好。我尝试重新安装和修复,但这没有帮助。这是整个错误消息: 1>------ Build starte
在我的代码的类部分,如果我写一个错误,则在不应该的情况下,将有几行报告为错误。我将'| error'放在可以从错误中恢复的良好/安全位置,但是我认为它没有使用它。也许它试图在某个地方恢复中间表情? 有
我遇到了 csv 输入文件整体读取故障的问题,我可以通过在 read_csv 函数中添加 "error_bad_lines=False" 来删除这些问题来解决这个问题。 但是我需要报告这些造成问题的文
在 Spring 中,验证后我们在 controller 中得到一个 BindingResult 对象。 很简单,如果我收到验证错误,我想重新显示我的表单,并在每个受影响的字段上方显示错误消息。 因此
我不知道出了什么问题,因为我用 Java 编程了大约一年,从来没有遇到过这个错误。在一分钟前在 Eclipse 中编译和运行工作,现在我得到这个错误: #A fatal error has been
SELECT to_char(messages. TIME, 'YYYY/MM/DD') AS FullDate, to_char(messages. TIME, 'MM/DD
我收到这些错误: AnonymousPath\Anonymized.vb : error BC30037: Character is not valid. AnonymousPath\Anonymiz
我刚刚安装了 gridengine 并在执行 qstat 时出现错误: error: commlib error: got select error (Connection refused) erro
嗨,我正在学习 PHP,我从 CRUD 系统开始,我在 Windows 上安装了 WAMP 服务器,当我运行它时,我收到以下错误消息。 SCREAM: Error suppression ignore
我刚刚开始一个新项目,我正在学习核心数据教程,可以找到:https://www.youtube.com/watch?v=zZJpsszfTHM 我似乎无法弄清楚为什么会抛出此错误。我有一个名为“Exp
当我使用 Jenkins 运行新构建时,出现以下错误: "FilePathY\XXX.cpp : fatal error C1853: 'FilePathZ\XXX.pch' precompiled
我是一名优秀的程序员,十分优秀!