Skip to content

Commit cd99f41

Browse files
UB26-005: Add -P to gnatprove args only if a project is set
1 parent c7c9b80 commit cd99f41

File tree

1 file changed

+15
-12
lines changed

1 file changed

+15
-12
lines changed

integration/vscode/ada/src/gnatproveTaskProvider.ts

Lines changed: 15 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ export default class gnatproveTaskProvider implements vscode.TaskProvider<vscode
5555

5656
// Arguments for proof of selected region need to be evaluated here
5757
if (definition.taskKind == taskKinds.proveRegion) {
58-
const args = getGnatproveArgs('${config:ada.projectFile}', ['-u', '${fileBasename}', '--limit-region=${fileBasename}:' + getSelectedRegion(vscode.window.activeTextEditor)]);
58+
const args = getGnatproveArgs(['-u', '${fileBasename}', '--limit-region=${fileBasename}:' + getSelectedRegion(vscode.window.activeTextEditor)]);
5959
const shell = new vscode.ShellExecution('gnatprove', args);
6060
return new vscode.Task(definition, vscode.TaskScope.Workspace, task.name, 'ada', shell, '$ada');
6161
}
@@ -67,7 +67,7 @@ export default class gnatproveTaskProvider implements vscode.TaskProvider<vscode
6767
.then(subprogram =>
6868
{
6969
let args = (definition.taskKind == taskKinds.examineSubprogram) ? ['--mode=flow'] : [];
70-
args = getGnatproveArgs('${config:ada.projectFile}', args.concat(['-u', '${fileBasename}', '--limit-subp=${fileBasename}:' + subprogram]));
70+
args = getGnatproveArgs(args.concat(['-u', '${fileBasename}', '--limit-subp=${fileBasename}:' + subprogram]));
7171
const shell = new vscode.ShellExecution('gnatprove', args);
7272
return new vscode.Task(definition, vscode.TaskScope.Workspace, task.name, 'ada', shell, '$ada');
7373
});
@@ -96,14 +96,14 @@ const getTasks = (): vscode.Task[] => {
9696
// Examine the project
9797
const examineProject = makeTask(
9898
taskKinds.examineProject,
99-
getGnatproveArgs('${config:ada.projectFile}', ['--mode=flow']),
99+
getGnatproveArgs(['--mode=flow']),
100100
'Examine project'
101101
);
102102

103103
// Examine the file
104104
const examineFile = makeTask(
105105
taskKinds.examineFile,
106-
getGnatproveArgs('${config:ada.projectFile}', ['--mode=flow', '-u', '${fileBasename}']),
106+
getGnatproveArgs(['--mode=flow', '-u', '${fileBasename}']),
107107
'Examine file'
108108
);
109109

@@ -117,14 +117,14 @@ const getTasks = (): vscode.Task[] => {
117117
// Prove the project
118118
const proveProject = makeTask(
119119
taskKinds.proveProject,
120-
getGnatproveArgs('${config:ada.projectFile}', []),
120+
getGnatproveArgs([]),
121121
'Prove project'
122122
);
123123

124124
// Prove the file
125125
const proveFile = makeTask(
126126
taskKinds.proveFile,
127-
getGnatproveArgs('${config:ada.projectFile}', ['-u', '${fileBasename}']),
127+
getGnatproveArgs(['-u', '${fileBasename}']),
128128
'Prove file'
129129
);
130130

@@ -145,7 +145,7 @@ const getTasks = (): vscode.Task[] => {
145145
// Prove the selected line line
146146
const proveLine = makeTask(
147147
taskKinds.proveLine,
148-
getGnatproveArgs('${config:ada.projectFile}', ['-u', '${fileBasename}', '--limit-line=${fileBasename}:${lineNumber}']),
148+
getGnatproveArgs(['-u', '${fileBasename}', '--limit-line=${fileBasename}:${lineNumber}']),
149149
'Prove line'
150150
);
151151

@@ -208,23 +208,26 @@ const getSelectedRegion = (editor: vscode.TextEditor | undefined): string => {
208208
}
209209
};
210210

211-
const getGnatproveArgs = (projectFile: string, args: string[]): string[] => {
211+
const getGnatproveArgs = (args: string[]): string[] => {
212212
// Append args (if any) and `-gnatef` to generate full file names in errors/warnings
213213
const p_gnatef = ['-cargs', '-gnatef'];
214-
return commonArgs(projectFile).concat(args, p_gnatef);
214+
return commonArgs().concat(args, p_gnatef);
215215
};
216216

217-
// return '-P project.gpr -XVAR=value` optiona
218-
const commonArgs = (projectFile?: string): string[] => {
217+
// return '-P project.gpr -XVAR=value` options
218+
const commonArgs = (): string[] => {
219219
const vars: string[][] = Object.entries(
220220
vscode.workspace.getConfiguration('ada').get('scenarioVariables') ?? []
221221
);
222222
const fold = (args: string[], item: string[]): string[] => {
223223
const option = '-X' + item[0] + '=' + item[1];
224224
return args.concat([option]);
225225
};
226+
226227
// Set projectFile is any
227-
const prj = projectFile ? ['-P', projectFile] : [];
228+
const prj = vscode.workspace.getConfiguration('ada').get(
229+
'projectFile') != "" ? ['-P', "${config:ada.projectFile}"] : [];
230+
228231
// for each scenarioVariables put `-Xname=value` option
229232
return vars.reduce(fold, prj);
230233
};

0 commit comments

Comments
 (0)